Skip to content

Improve quality#88

Draft
mikucionisaau wants to merge 54 commits into
UPPAALModelChecker:mainfrom
mikucionisaau:improve-quality
Draft

Improve quality#88
mikucionisaau wants to merge 54 commits into
UPPAALModelChecker:mainfrom
mikucionisaau:improve-quality

Conversation

@mikucionisaau

@mikucionisaau mikucionisaau commented Jul 9, 2026

Copy link
Copy Markdown
Member
  • fixed namespace issues
  • added CMake presets for sanitizers and code coverage
  • added scripts to generate coverage reports using lcov, gcovr and llvm-cov
  • added tests to improve test coverage
  • fixed clang-tidy warnings
  • fixed flex scan memory leak when an exception is thrown
  • fixed crash in Location::print and Edge::print when missing labels
  • fixed crash in Expression::print when empty
  • fixed LSC region printing when empty

mikucionisaau and others added 30 commits July 7, 2026 16:39
…al library file before executing external function test
Documents the CMake preset workflow, single-test invocation, and the
parser/builder/document architecture for future Claude Code sessions.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
AbstractBuilder gives every ParserBuilder method a "not supported"
default except expr_MITL_diamond/expr_MITL_box, which stayed pure
virtual and happened to be masked by every existing subclass
overriding them. Add the same default for consistency, and add
abstractbuilder_test to exercise every inherited method, which takes
src/AbstractBuilder.cpp from 2% to 100% line coverage.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
PrettyPrinter had 0% test coverage because prettyprint_test.cpp only
exercises Expression::str()/Document printing, not the PrettyPrinter
builder itself (used by the `pretty` CLI tool). Add
PrettyPrinter_test.cpp driving it through parse_XML_buffer/parse_property
against real and synthetic models, covering types, declarations,
structs/arrays/strings, all loop forms, expression operators, template
printing (rates, invariants, guards, urgent/committed/branchpoint/select/
sync), and the SMC/MITL/CTL callbacks that only run before their
enclosing (unimplemented) property()/expr_MITL_formula() throws.

While building the fixtures, found two real bugs:
- decl_external_func() was a no-op, so the `param` string accumulated
  by decl_parameter() (and the external function's return type) leaked
  into the next process's printed parameter list.
- do_while_begin()/do_while_end() were no-ops, silently dropping a
  do-while loop's body and condition from the output entirely.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
typeexception.cpp's 11 TypeException factory functions had no direct
tests. print.hpp (print_infix/infix) is unused elsewhere except one
call site in DocumentBuilder.cpp, and being header-only its templates
need their own test binary instrumented for coverage to show at all
-- add target_coverage(print_test) since only the UTAP library target
was instrumented before.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
parse_XTA/parse_property called scan buffer -> parse -> delete buffer
sequentially, so an exception thrown by the ParserBuilder mid-parse
(an explicitly documented way to report errors, see builder.hpp)
skipped the delete and leaked the flex buffer. Surfaced by
AddressSanitizer once PrettyPrinter_test.cpp added the first tests
that parse through a builder expected to throw. Fix with a small RAII
guard so the buffer is always freed, even on the exception path.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
These were the only StatementBuilder methods defined inline in the
header instead of in StatementBuilder.cpp like the rest of the class.
Being trivial but virtual, the compiler emits weak-linkage copies in
every including translation unit; gcov's coverage data ends up split
across the copies the linker discards, showing 0% even though the
methods run on every if-statement. Moving them to the .cpp (matching
the class's own convention) fixes the attribution and gets them to
100% via the existing if_statement.xml parsing test.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…mented

utap.hpp declared `expression_t parse_expression(const char*, Document&,
bool)`, but expression_t was only ever forward-declared (symbols.hpp)
and never defined, and no .cpp anywhere implemented parse_expression --
any caller would hit a linker error. Meanwhile TypeChecker.cpp had a
fully working parseExpression() (camelCase) doing the real work, just
never declared in any public header. This looks like a half-finished
rename. Fix by renaming the working implementation to parse_expression
and declaring it with its actual return type (Expression), and drop the
now-unused expression_t forward declaration.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
errors, expression type errors, and Document-based parse entry points

Adds 20 test cases found by working empirically: TypeChecker only runs
when the document has no earlier (parser/builder-level) errors, so
many error-message factory functions need a document that is otherwise
clean but semantically wrong in one specific way. Covers:
- assert/empty/for/range-iteration/do-while statement visitors, none
  of which were exercised by any existing test
- 5 type-prefix errors (meta/const/urgent/broadcast misuse), reachable
  only through a typedef'd clock since the grammar has no direct
  `TypePrefix T_CLOCK` production
- 10 expression-level type errors (invalid assignment, wrong argument
  count, unknown struct field, etc.)
- parse_XTA(const char*), parse_XTA(FILE*), parse_XML_fd, and the
  newly-fixed parse_expression, none of which any existing test called

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Struct initializer errors (multiple initialisers for a field, too many
elements) and the dynamic-template spawn checks (spawning a declared-
but-undefined template, and doing so outside an edge update, both of
which fire together from a single spawn-in-a-function-body call).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
E[...](min:...), Pr[...](<> ...), probability comparison, quantitative
threshold comparison and simulate[...] queries, parsed via
parse_property and type-checked through the QueryBuilder pattern
(document_fixture.h). These exercise checkNrOfRuns,
checkBoundTypeOrBoundedExpr, checkBound, checkAggregationOp,
checkMonitoredExpr, checkPredicate, checkUntilCond, checkPathQuant and
checkProbBound, none of which were reachable from the document_fixture-
only tests added so far since they only run inside a property/query,
not a plain document.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Edge-level checks (guard must be side-effect free, sync must be a
channel, both needing a custom template with a real transition since
document_fixture's default template has none), iteration-variable type
checks, array-initialiser field-name misuse, sum-expression body type
checks, and progress-measure guard/measure type checks (built via a
raw XML document since document_fixture::add_system_decl() inserts
text before the `system X;` line, but progress must follow it per the
grammar: System: SysDecl Progress GanttDecl).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Array-index/comma-expression type mismatches, a reference-parameter
template instantiation given a non-unique-reference argument
(exercises isUniqueReference), and a fully-defined dynamic template
spawned on an edge with matching arguments (exercises
checkSpawnParameterCompatible's success path).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…r.cpp

Covers: urgent edges with clock guards / strict bounds, broadcast input
edges into branchpoints (must be deterministic) and into locations with
a non-true invariant, mixing CSP-style and IO-style channel
synchronisation on the same template, and the three refinement-only
warnings (uncontrollable output, controllable input, CSP sync
incompatible with refinement) -- these last three only fire when
TypeChecker is constructed with refinement=true, which
static_analysis() (used by every parse_XTA/parse_XML_* overload) never
does, so those tests re-visit an already-parsed Document with a
refinement-enabled checker directly.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
property.cpp/property.hpp were at 27%/5% coverage because the only
existing consumers of PropertyBuilder's real pipeline (via
document_fixture's QueryFixture/TigaPropertyBuilder) were a handful of
query forms in prettyprint_test.cpp (E<>, Pr[...] comparisons,
simulate, saveStrategy); every other query form used the local
lightweight QueryBuilder class instead, which overrides property() to
just stash the expression and skip typeProperty() entirely.

Adds tests for the quant_t classification of A[]/E[]/A<>/-->/
sup{}/inf{}/bounds{}, the SMC probability-threshold and MITL forms,
the TIGA control-synthesis forms (control:, E<> control:, minE/maxE),
the deadlock-predicate and dynamic-template restrictions in
property(), handle_expect()/parseExpect()'s status/time/memory token
parsing (a fully public but otherwise uncalled-from-anywhere API), and
the duplicate-strategy-declaration/undeclared-strategy-subjection
checks in TigaPropertyBuilder.

Also found along the way: parser.y's CALL() macro catches any
TypeException thrown from a builder callback and converts it into a
recorded document error via handle_error(), so PropertyBuilder's
`throw TypeException{...}` calls never propagate as C++ exceptions
during normal parsing -- only document_fixture's QueryFixture
re-throws as std::logic_error, and only because it explicitly checks
doc.get_errors() itself after the parse call returns.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…nctions

Covers pre-decrement, the three built-in-math-function arities, global
vs. template-local scalar[] declarations (the latter exercising
collect_dependencies(), which only runs when a scalar set's size is
declared inside a template), the control_t* time-optimal synthesis
form (expr_ternary, also fixing property.cpp's CONTROL_TOPT gap),
numOf()/foreach() (both throw a later type/lookup error but the
builder callback itself already ran), forall/exists/sum over a
properly-defined dynamic template (also covers push/pop_dynamic_frame_of
transitively), and the MITL until/release/box/next forms.

Also adds one property.cpp test: PropertyBuilder::scenario() throws a
raw std::runtime_error (not TypeException), so unlike other
PropertyBuilder checks it is NOT caught by parser.y's CALL() macro and
propagates directly out of parse_property() -- this also means
expr_scenario(), the next callback in the same grammar rule, likely
never runs when scenario() rejects its argument, so it's still
uncovered pending a full LSC template fixture.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Both unconditionally called .print() on their invariant/exp_rate (resp.
guard/sync/assign) Expression members, but Expression::print()
dereferences a null internal pointer for an empty Expression --
crashing for the extremely common case of a location with no
invariant/rate, or an edge missing any of guard/sync/assign. Neither
method had ever been exercised by any test, which is why this went
unnoticed. Guard each call with .empty(), matching the style already
used in Variable::print()'s "if (!init.empty())".

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Template/Instance/ChanPriority members

Covers find_template, get_dynamic_templates, queries_empty,
get_options/set_options, get_proc_priority (via a system-level "P1 <
P2" priority ordering), remove_process, copy_variables_from_to (plus
a bare call to copy_functions_from_to, currently an intentional no-op),
add_gantt (built via a raw XML document since document_fixture's
add_system_decl() inserts text before the `system X;` line, but gantt
must follow it per the grammar), add_io_decl, ChanPriority::print/str,
Location::print/str and Edge::print/str (the two crash fixes from the
previous commit), Variable::str/Function::str/Declarations::str,
Template::is_invariant (via a minimal LSC template), and
Instance::arguments_str/mapping_str/print_arguments/print_mapping (via
a parameterized template instantiation).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…ents

model_options() used begin(Tag::OPTION) with the default skipEmpty=true,
silently skipping self-closing <option key="..." value="..."/> tags in
<queries>, unlike query_options()'s option() which correctly passes false.

expectation() never called read() to descend past the <expect> start tag
before scanning for <resource> children, so begin(Tag::RESOURCE, false)
always saw the still-current <expect> element and returned false
immediately -- any <resource> children were silently dropped.

Both functions also leaked the key/value/outcome/type/value attribute
strings returned by getAttribute(), which the caller must xmlFree().
…arts

Covers before_update/after_update declarations, gantt chart select clauses
(declaration-level and for-select), edge probability labels, model-level
and per-query options, query expectations with nested resources, and the
otherwise-unreachable query_results_begin/end. Includes regression tests
for the model_options()/expectation() parsing fixes.
operator<<(ostream&, const Error&) streamed e.start.path (a
shared_ptr<string>) directly, invoking shared_ptr's own operator<< and
printing the raw pointer address instead of the path text -- unlike the
parallel Error::str(), which correctly dereferences it. Both now agree.
Covers add()/find() monotonicity and empty-index error paths, the
binary search across more than two lines, Error::str()/operator<<
agreement with and without a path, the "Unknown position" fallback,
and PositionIndex::print(). Includes a regression test for the
operator<< path-pointer fix.
print() dereferenced the internal pImpl data unconditionally, so calling
str() (documented to "return empty if the expression is empty") or
print() directly on a default-constructed Expression crashed. document.cpp
already guards its callers (Location::print/Edge::print) against this, but
any other caller -- including future ones -- would still hit it. Guard in
print() itself, matching the documented contract.
The header declared operator<<(ostream&, const Symbol&) and the Frame
overload in the global namespace, while symbols.cpp defined them inside
namespace UTAP -- two distinct, mismatched entities. Ordinary lookup found
the (never-defined) global declaration ahead of ADL, so any code that
triggered it, such as a generic stringifier for a Symbol, failed to link.
Declare both as hidden friends of their respective classes instead, tying
them to the same namespace as their definitions.
Extends the existing Expressions test suite with: clone()/clone_deeper()/
subst(), arithmetic/logic/comparison/ternary/quantifier/builtin-function
printing (via parse_expression), assignment/increment/array/record/
function-call/sync/clock-rate printing (via document_fixture models),
uses_fp/uses_hybrid/uses_clock, deadlock/exit and is_dynamic/
has_dynamic_sub, get_symbol/get_symbols across expression kinds, and
changes_variable/depends_on/is_reference_to. Includes regression tests
for the print()-on-empty-expression and Symbol/Frame operator<< fixes.
add_variable()/add_function() passed an already-suffixed string to
NotSupportedException, which itself appends " is not supported" -- every
other call site in the codebase (via the UNSUPPORTED macro) passes just
the bare function name. Produced "add_variable is not supported is not
supported" instead of the intended message.
… case

A simregion has "1 or 0" of {message, update, condition} by design (see
Template::get_simregions()'s own doc comment), so a message-only simregion
has a null .update and .condition, an update-only one has a null .message
and .condition, etc. LSCInstanceLine::get_simregions() dereferenced all
three unconditionally, crashing on any simregion that wasn't a full
message+update+condition triple -- the common case in practice.
…scenarios

Covers Location/Edge print with exponential-rate/synchronisation labels,
multi-parameter Function/Instance printing, duplicate location/branchpoint
name errors, a branchpoint used as an edge source, ChanPriority's default
keyword, and a full LSC scenario (messages, conditions, updates across
four instance lines) exercising Template::get_simregions(), both
get_update() overloads, LSCInstanceLine::get_simregions(), LSCSimRegion
and LSCCut. Includes a regression test for the LSCInstanceLine
null-dereference fix.
Covers location rendering (Err color, urgent, exponentialrate),
self-loop transitions, channel priority declarations, renamed process
instantiation, LSC templates being skipped on write, and the
write_XML_file() failure path when the output path can't be opened.
These were defined inline in the header (either as one-line bodies inside
the class definition, or as free-standing "inline" functions after the
class), so each translation unit that includes statement.hpp got its own
weak-symbol copy. gcov's coverage attribution doesn't reliably merge
across those duplicate copies, so lines that were clearly being executed
(confirmed via existing tests calling .returns()/.accept() directly)
showed as 0% covered. Matches the same fix already applied to
StatementBuilder.hpp earlier. No behavioral change.
Adds returns()/accept() coverage for EmptyStatement, CaseStatement,
DefaultStatement, BreakStatement and ContinueStatement, a
collect_changes()/collect_dependencies() case exercising switch/case/
default via ExpressionVisitor, and a direct AbstractStatementVisitor
dispatch test covering every statement kind. The switch/case/break/
continue classes are exercised via direct construction rather than
parsing: "switch", "case", "break" and "continue" are not registered as
lexer keywords (only "default" is, for the unrelated "chan priority
default" syntax), so that whole statement form is unreachable from any
real model despite the grammar productions and builder callbacks existing
end-to-end.
@mikucionisaau mikucionisaau force-pushed the improve-quality branch 4 times, most recently from 8912484 to 547ceb7 Compare July 10, 2026 12:24
The error branch unconditionally referenced iodecl.csp.front(), but when
the mismatch is triggered by *this* iodecl's inputs/outputs (having
followed a previous CSP-style iodecl), its own csp list is empty --
.front() on that empty std::list is undefined behavior. Pick whichever of
csp/inputs/outputs is actually non-empty for this iodecl.
Unlike every other compound-assignment operator (-=, /=, %=, *=, &=, |=,
^=, <<=, >>=), which return false immediately after reporting a type
error, ASS_PLUS fell through to assign a type and reached the end of
checkExpression's default success path -- so "x += <bad-rhs>;" or
"<non-lvalue> += 1;" still reported checkExpression()==true downstream
despite the recorded error, inconsistent with the sibling operators.
Covers checkType (reference/range/string/committed-location checks),
priority declarations (array/indexed channels), visit_process's unbound-
parameter checks, visit_variable/visit_location/visit_edge error paths
(invariant/guard/probability type and side-effect checks, CSP-then-IO
sync ordering), LSC message/condition error branches, visit_instance
argument-compatibility branches, visitProperty error branches,
checkObservationConstraints's clock-bound checks, statement-visitor
side-effect/range checks, parameter-compatibility gaps, the ternary
operator's record/equivalent-type fallbacks, spawn/numOf/exit, forall/
exists/sum's non-boolean result types, comma/array-index edge cases,
isUniqueReference's identifier/dot/array success arms, and IODecl's
type-checking (constructed directly, since "IO" is a registered keyword
with no grammar production that ever consumes it).

Includes regression tests for both TypeChecker fixes: visit_io_decl's
crash on an empty csp list, and ASS_PLUS's missing return false.
std::filesystem::remove() while an ifstream on the same path is still
open throws a sharing-violation error on Windows (POSIX allows it).
Close the stream explicitly before removing the temp file.
may_need_guard_involving_target_invariant is only emitted inside an
#ifndef NDEBUG block in visit_edge, so it never fires in Release
builds (e.g. the mingw cross-compile, which defaults to Release).
Skip the assertion in that configuration instead of failing.
mikucionisaau and others added 11 commits July 10, 2026 16:01
libxml2's dict.c calls BCryptGenRandom, which needs -lbcrypt. The
mingw cross-compile toolchains already carry this workaround via
LIBXML_WINLIBS; the native x86_64-windows-gcc/clang toolchains (used
by msys2 ucrt64 builds) were missing it, causing an undefined
reference when linking pretty/syntaxcheck/featurecheck.
The test hardcoded the OS-supplied suffix of Windows errors 126/127,
but that text differs between real Windows ("The specified module
could not be found.") and Wine's FormatMessage emulation ("Module not
found."), so no single string matched both. Only assert on the parts
we control (our own prefix text and the error code).
`expr` was a reference into `fragments.data`; calling `expr.get_type()`
after `fragments.pop(2)` read from ASan-poisoned container-overflow
memory. Save the type into a local before the pop.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
line.path is a shared_ptr<string>; streaming it directly prints the
raw pointer value rather than the path text. This was masked on
libstdc++, where a null pointer streams as "0", but on libc++ (macOS)
it streams as "0x0", causing position_test to fail there. Dereference
the pointer (or print empty for null) instead. Added a test case with
a non-null path, since the previous test only ever exercised nullptr.
Bison's generated parser.cpp defines constants like YYPURE, YYPUSH,
YYPULL as macros, which we don't control and can't rewrite as
constexpr. Same treatment as the existing yy_sname naming exception.
….cpp

Bison's stack-growth cleanup frees yyss only when it was heap-reallocated,
but GCC's alias analysis can't always prove that, producing a false
positive on the stack-local yyssa fallback array. Scoped to the generated
parser.cpp translation unit only, GCC only.
- Add "debug", "release", "debug-san", "release-san" as configure
  preset aliases of "multi"/"multi-san" (in cmake/CommonPresets.json),
  matching the existing build/test/workflow preset names of the same
  configuration so they no longer need "multi" to be remembered
  separately for configuring.
- Rename the "quick" build/workflow presets for consistency:
  quick-release      -> release-quick
  quick-debug        -> debug-quick
  quick-release-san  -> release-quick-san
  quick-debug-san    -> debug-quick-san
  All now follow the same "<config>[-quick][-san]" ordering. Updated
  the CI workflows that invoked "quick-release" by name.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant