Rebase cex analysis#7

Open

peterschrammel wants to merge 84 commits intomasterfrom

Commits on May 3, 2017

all commits of old branch

Peter Schrammel
authored and
peterschrammel
committed
all commits of old branch

Peter Schrammel
authored and
peterschrammel
committed
all commits of old branch

Peter Schrammel
authored and
peterschrammel
committed
fixed compilation errors after merge

Peter Schrammel
authored and
peterschrammel
committed
use cex analyser concrete with --inline

Peter Schrammel
authored and
peterschrammel
committed
made sure that the executable is named 2ls

Peter Schrammel
authored and
peterschrammel
committed
bug fixes for abstract case

kumarmadhukar
authored and
peterschrammel
committed
loop-specific unwinding code, in progress

kumarmadhukar
authored and
peterschrammel
committed
commented new code to check loop-specific unwinding

kumarmadhukar
authored and
peterschrammel
committed
commented debug code

kumarmadhukar
authored and
peterschrammel
committed
put unwinding suffix into ID_suffix attribute

Peter Schrammel
authored and
peterschrammel
committed
collect nondet vars in local_SSA

Peter Schrammel
authored and
peterschrammel
committed
add nondets as OUT vars to summary template for backwards analysis

Peter Schrammel
authored and
peterschrammel
committed
fixed various places where nondet_symbols in templates were not expected

Peter Schrammel
authored and
peterschrammel
committed
added a comment for new fields in loopt

kumarmadhukar
authored and
peterschrammel
committed
fixes to replace_globals when inlining

Peter Schrammel
authored and
peterschrammel
committed
nondet locals only once

Peter Schrammel
authored and
peterschrammel
committed
fixed filtering of non-violating assertion instances before running spurious checker; various code clean-ups

Peter Schrammel
authored and
peterschrammel
committed
modified loop-specific unwinder to iterate over all loops

kumarmadhukar
authored and
peterschrammel
committed
selective unwinding code

kumarmadhukar
authored and
peterschrammel
committed
output unsat core for spurious cex, uses incremental solver debug facilities at the moment

Peter Schrammel
authored and
peterschrammel
committed
Srivas' examples

Peter Schrammel
authored and
peterschrammel
committed
moved assertion into bar()

Peter Schrammel
authored and
peterschrammel
committed
recompute dependency graphs after unwinding

Peter Schrammel
authored and
peterschrammel
committed
fixed renaming of nondets on inlining

Peter Schrammel
authored and
peterschrammel
committed
propagate nondets in error summaries up to entry point

Peter Schrammel
authored and
peterschrammel
committed
fixed use of ssa_expr in trace output

Peter Schrammel
authored and
peterschrammel
committed
minor bug fixes

kumarmadhukar
authored and
peterschrammel
committed
unsat core output (without using incremental solver debug mode)

Peter Schrammel
authored and
peterschrammel
committed
get reason for spuriousness

Peter Schrammel
authored and
peterschrammel
committed
to start with, add all functions and loop ids to reason

Peter Schrammel
authored and
peterschrammel
committed
reason grouped by functions; identify callee by call site location

Peter Schrammel
authored and
peterschrammel
committed
selective unwinding and inlining code - in progress

kumarmadhukar
authored and
peterschrammel
committed
code for unwinding and inlining

kumarmadhukar
authored and
peterschrammel
committed
minor fix in inlining code

kumarmadhukar
authored and
peterschrammel
committed
more k-induction tests

Peter Schrammel
authored and
peterschrammel
committed
spurious check refactoring started

Peter Schrammel
authored and
peterschrammel
committed
refactoring done, except loop continuations

Peter Schrammel
authored and
peterschrammel
committed
loop-specific continuation conditions

Peter Schrammel
authored and
peterschrammel
committed
update enable_expr after 0th unwinding

Peter Schrammel
authored and
peterschrammel
committed
concrete only complete with inline

Peter Schrammel
authored and
peterschrammel
committed
take into account enabling_expr in depgraph construction

Peter Schrammel
authored and
peterschrammel
committed
fixed all no-cex regressions for complete

Peter Schrammel
authored and
peterschrammel
committed
factor out SSA refinements into separate classes

Peter Schrammel
authored and
peterschrammel
committed
unwind output one-off

Peter Schrammel
authored and
peterschrammel
committed

Commits on May 4, 2017

flag functions as inlined and debug output in ssa_refiner about what is being refined

Peter Schrammel
authored and
peterschrammel
committed
recursive gathering of summaries and inlined functions

Peter Schrammel
authored and
peterschrammel
committed
basic unsat-core based refinement selection

Peter Schrammel
authored and
peterschrammel
committed
fully-unwound check fixed as far as possible

Peter Schrammel
authored and
peterschrammel
committed
unwind value propagation bug fixed (#5)

kumarmadhukar
authored and
peterschrammel
committed
check whether function has assertion was too semantic, we needed to set the property map correctly

Peter Schrammel
authored and
peterschrammel
committed
loop enabling expr fixed

Peter Schrammel
authored and
peterschrammel
committed
loop enabling expr fixed, removed superfluous variables

Peter Schrammel
authored and
peterschrammel
committed
missing regressions

Peter Schrammel
authored and
peterschrammel
committed
simplified example that exposes problem with monolithic --k-induction --havoc

Peter Schrammel
authored and
peterschrammel
committed
wrong assertions feeded into cex checker; output assignments in incremental_solver debug mode

Peter Schrammel
authored and
peterschrammel
committed
collecting renamed error assertions - still some of them are missed

Peter Schrammel
authored and
peterschrammel
committed
assertion renaming in cex_complete fixed

Peter Schrammel
authored and
peterschrammel
committed
be more robust w.r.t. functions that are not in the SSA db

Peter Schrammel
authored and
peterschrammel
committed
assumptions must hold in backwards analysis

Peter Schrammel
authored and
peterschrammel
committed
clean up summary_checker_base

Peter Schrammel
authored and
peterschrammel
committed
check for inlined functions whether they have assertions

Peter Schrammel
authored and
peterschrammel
committed
recursively collect assertions from inlined functions through inliner

Peter Schrammel
authored and
peterschrammel
committed
sync

Peter Schrammel
authored and
peterschrammel
committed
depgraph renaming problem fixed

Peter Schrammel
authored and
peterschrammel
committed
inlined functions must not contain negated assertions; assertions are added separately

Peter Schrammel
authored and
peterschrammel
committed
regression tests refactored

Peter Schrammel
authored and
peterschrammel
committed
partial upgrade to new cbmc version

Peter Schrammel
authored and
peterschrammel
committed
bounds simplification
peterschrammel
committed
merge

Peter Schrammel
authored and
peterschrammel
committed
merge

Peter Schrammel
authored and
peterschrammel
committed
bounds simplification
peterschrammel
committed

Commits on May 9, 2017

Rebase bw cex
peterschrammel
committed

Commits on May 11, 2017

Improved gitignore
peterschrammel
committed

Commits on May 14, 2017

Clean up
peterschrammel
committed

Commits on Jun 2, 2017

Spurious checker needs entry point function and goals need expression
peterschrammel
committed

Commits on Jun 7, 2017

Commits on Jun 8, 2017

Commits on Jun 10, 2017

Fixed incorrect result from summarizer_bw_cex_concrete
rnbguy
committed

Commits on Jun 22, 2017

Merge pull request #10 from rnbdev/comp-kind-fixes
peterschrammel
authored

Commits on Jun 29, 2017

fixed spurious-check options

kumarmadhukar
authored and
peterschrammel
committed