gradual-verification silicon-gv issues

gradual-verification / silicon-gv

Mozilla Public License 2.0

0 stars 3 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Modifications for debugger support

#58 advancingdragon closed 2 weeks ago
0
Minor changes to improve source line and column position reporting.

#57 advancingdragon closed 3 months ago
0
Not producing run time checks for unfolds with predicates not in the heap/optimistic heap

#56 jennalwise closed 1 year ago
1
Default missing specifications to ? not true

#55 jennalwise opened 1 year ago
0
Regex should be last resort for translation

#54 jennalwise closed 1 year ago
1
Frame checks for loop condition at end of loop body are implemented incorrectly; leading to dereferencing of null pointers

#53 jennalwise closed 1 year ago
1
Checks for framing loop conditions after the loop do not attach After loop tags to short-circuiting conditions during the conditions eval

#52 jennalwise closed 1 year ago
1
Partitioning predicates for smarter runtime check assertions

#51 janpaulpl opened 1 year ago
1
VariableResolver in Translator entering infinite loop during Composite gradual verification

#50 jennalwise closed 2 years ago
1
Consume evalandassert not handling failure return from evalpc

#49 jennalwise closed 2 years ago
1
initial opt for issue-35; opt perms for framing added to OH in produce

#48 jennalwise closed 2 years ago
0
Issue46

#47 jennalwise closed 2 years ago
0
Unable to match type for Null during static verification of avlja.c0

#46 icmccorm closed 2 years ago
3
Translator may give back expressions from the path condition that are dropped due to heap location modification

#45 jennalwise opened 2 years ago
0
Translator does not return the expression with the shortest dereference path

#44 jennalwise closed 2 years ago
1
Issue42

#43 jennalwise closed 2 years ago
0
Unfold of predicates inefficient, can be improved by preserving argument framing in OH

#42 jennalwise closed 2 years ago
3
Fixes for Issue38 & Issue40

#41 jennalwise closed 2 years ago
0
Translating run-time checks from asserts with wrong state

#40 jennalwise closed 2 years ago
3
After a loop, imprecision from before the loop and residuals from consumption need to be joined with the invariant

#39 jennalwise closed 2 years ago
1
IndexOutOfBounds triggered by Translator.selectShortestField

#38 icmccorm closed 2 years ago
3
Heap chunk removal is more efficient for certain orderings of information in specs

#37 jennalwise opened 2 years ago
0
Better abstraction for state merging for the OH

#36 jennalwise opened 2 years ago
0
Heap location tracking in produce is resulting in too many run-time checks

#35 jennalwise opened 2 years ago
0
Framing runtime checks should be emitted at the end of each loop iteration

#34 hgouni closed 2 years ago
1
The translator should always return the shortest available field name

#33 hgouni closed 2 years ago
1
Regex Handler in Translator needs to handle cases like (Second: $t@10@01).Node$total@20@01

#32 jennalwise closed 2 years ago
1
Backend not printing run-time checks

#31 jennalwise closed 2 years ago
1
Infinite loop when resolving variables.

#30 icmccorm closed 2 years ago
2
Store.getKeyForValue should not be called with non-variable types, Related to Issue https://github.com/gradual-verification/silicon-gv/issues/25

#29 jennalwise closed 2 years ago
1
Static profiler reporting incorrect numbers for full static solution in list.c0 and for predicate_vars.c0

#28 jennalwise closed 2 years ago
2
Short Circuiting Eval is Producing Run-time Checks in Produce

#27 jennalwise closed 2 years ago
3
If/Loop branch conditions using wrong position information

#26 jennalwise closed 2 years ago
1
Run-time checks/branch conditions based on predicate bodies/method contracts use declaration variable not current context variable

#25 jennalwise closed 2 years ago
2
ChunkSupporter.consume not using correct heap unless consolidating

#24 jennalwise closed 2 years ago
1
getEquivalentVariables needs to check that the term is in fact a variable in the PC

#23 jennalwise closed 2 years ago
3
Translating Branch Conditions w/ Wrong State

#22 jennalwise closed 2 years ago
3
Translator bug: Could not translate term into Viper expression for check!

#21 jennalwise closed 2 years ago
1
State merging failed: unexpected mismatch between symbolic states

#20 jennalwise closed 2 years ago
1
Branching fix for adherence to gradual guarantee

#19 jennalwise closed 2 years ago
1
Explore checkSmoke paths through static verification (aka. infeasible paths)

#18 jennalwise opened 2 years ago
2
Fix consumeGreedy based on fixes to heap-rem in sym-exec document

#17 jennalwise closed 2 years ago
1
Look into restricting top-level verification of functions

#16 jennalwise opened 3 years ago
0
Reassignment of a variable using a previous value of that variable results in false path condition terms

#15 hgouni closed 3 years ago
2
Support joins during runtime check collection across branches

#14 hgouni opened 3 years ago
2
Eval contains cases for unsupported features

#13 jennalwise closed 3 years ago
1
Eval-pc missing default match case that maps to featureunsupported exception

#12 jennalwise closed 3 years ago
1
Need to reset state to before the assert after the well-formed check in the assert computation

#11 jennalwise closed 3 years ago
1
Consume eval & assert case missing reassignment of imprecise state boolean

#10 jennalwise closed 3 years ago
1
ChunkSupporter.consume no longer uses ve: VerifierError argument

#9 jennalwise opened 3 years ago
0