search

imitator-model-checker / imitator

IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.
https://www.imitator.fr/
GNU General Public License v3.0
26 stars 12 forks source link

The syntax of unused functions is not checked #203

Open himito opened 5 days ago

himito commented 5 days ago

Description

When a function is not used, its syntax is not checked. It is tested in the benchmark 30

Reproduce

./bin/imitator -mode checksyntax  tests/testcases/functions/unused-function-invalid-syntax.imi

The file unused-function-invalid-syntax.imi contains an automaton with a function with syntax errors: 

function this_function_does_nothing () : bool
begin
  return this_does_not_exist(some_unknown_variable) + toto * (hello (hello))
end
himito commented 5 days ago

A clue is the file ModelConverter.ml

https://github.com/imitator-model-checker/imitator/blob/b446b90140cfdf70d496016ea0e6439e7141acbc/src/lib/ModelConverter.ml#L3486

We could try to convert all the functions instead of only the used ones