symdivine ltl error

[nisrine]

Hi, I got the same error as an input for all the models that I've tried when trying to verify LTL property. which is:

Unknown token! terminate called after throwing an instance of 'std::runtime_error' what(): ERROR: syntax error, unexpected $end Aborted (core dumped)

And for the reachability for one of my models I got this output

symdivine: /home/nisrine/SymDIVINE-master/src/llvmsym/memorylayout.h:133: void llvm_sym::MemoryLayout::setMultival(llvm_sym::MemoryLayout::VariableId, bool): Assertion `variable.segmentId < variablesFlags.size()' failed. Aborted (core dumped)

Any help please, thank you.

[yaqwsx]

Hi, the first error marks you have invalid syntax in your LTL fromula. Could you send it?

The second error is related to #6, are you using pointers in your program?

[nisrine]

Hi, thanks for your quick response. My LTL formula is : (G((updateSM = PENDING) => F (updateSM == PROCESS))) For the second one no I'm not using pointers in my program

[yaqwsx]

Atomic proposition has to be enclosed in [] and has to refer to global variables (global variables are named seg1_off{x}, where {x} is their index in bitcode file). So your formula should look like this: (G([seg1_off0 = 0(32)] => F [seg1_off1 = 1(32)])).

[nisrine]

Hi, I still get the same error even after the modification of the property. I've also tried with a very basic C program, and I have the same error. also in the examples in the zip attached symDivine.tar.gz

[yaqwsx]

There are the same examples with their properties written in property.ltl file. ltl.zip

[nisrine]

Please check if I'm using the correct model in this example

:~/SymDIVINE-master$ bin/symdivine reachability ../Downloads/ltl/afp-succeed/model_op.ll Safe. nisrine@nisrine:~/SymDIVINE-master$ bin/symdivine ltl ../Downloads/ltl/afp-succeed/property.ltl ../Downloads/ltl/afp-succeed/model_op.ll Unknown token! terminate called after throwing an instance of 'std::runtime_error' what(): ERROR: syntax error, unexpected $end Aborted (core dumped)

[yaqwsx]

bin/symdivine ltl  `cat ../Downloads/ltl/afp-succeed/property.ltl` ../Downloads/ltl/afp-succeed/model_op.ll

[nisrine]

As an ouput for the command I got :

Unexpected argument: ltl, cat, ../Downloads/ltl/afp-succeed/property.ltl, ../Downloads/ltl/afp-succeed/model_op.ll SymDIVINE.

Why you added cat ?

[yaqwsx]

GitHub escaped quotes - I updated the comment.

[nisrine]

First thanks a lot for your help, but still not working. For the example I got

:~/SymDIVINE-master$ bin/symdivine ltl \cat ../Downloads/ltl/afp-succeed/property.ltl../Downloads/ltl/afp-succeed/model_op.ll bash: ../Downloads/ltl/afp-succeed/model_op.ll: Permission denied ../Downloads/ltl/afp-succeed/property.ltl: ../Downloads/ltl/afp-succeed/property.ltl:1:2: error: expected integer !(F([seg1_off0 != 0(32)])) ^

I also tried on my program and got:

:~/SymDIVINE-master$ bin/symdivine ltl \cat prop.ltlmain.ll main.ll: command not found prop.ltl: prop.ltl:1:1: error: expected top-level entity (G([updateSM = 601] => F [updateSM = 602])) ^

What do you think it is related to?

Thanks again