String solver #252
String solver #252
Conversation
- added more operations to the SMT-LIB string theory - added an alternative backend using quantifiers and arrays instead of the string theory still work in progress
these show that, as expected, conversion BV<->INT introduces huge performance problems
this is quite quick also with the INT<->BV conversion
…e before re-generating)
…xiom instantiation) Only stubs so far
The code now compiles, but it is not yet reachable from main (so, completely untested...)
unfortunately, this is still broken
…g for axiom violations is still broken (don't know why though)
…tion of the c tests accordingly
…an expression that should be added to the index set
…aving a variable appear several time in the same expression
…e appear several time in the same expression
…e appear several time in the same expression
…e appear several time in the same expression
|
May I ask you to split this up?
|
|
I tried to split the changes as you suggested, and there is an additional one (between 4 and 5) that contains the changes in goto-programs. Each pull request should contain a commit independent from the others. I hope this is fine like this. Romain From: Daniel Kroening [email protected] May I ask you to split this up?
You are receiving this because you authored the thread. |
SEC-96 Tests for LVSA precise access paths
Fix write_stack to correctly complete types for index_exprt expressions
This is a possible pull for integrating the string solver in CBMC.
I've tried to keep the changes outside newly created files to a minimum.
The only compatibility problem that I can see is the conversion between utf8 and utf16 that I'm using for unicode strings, it uses a function that may not be available to old version of gcc (before gcc-5 it seems).
Otherwise when the --pass option is not activated, the behavior of CBMC should be exactly the same as before.