diff --git a/analyzer.ml b/analyzer.ml index b6b0cd9..db22a43 100644 --- a/analyzer.ml +++ b/analyzer.ml @@ -23,6 +23,7 @@ let doit filename = begin | "constants" -> if !Options.disjunction then ConstDisjIterator.iterate cfg else ConstIterator.iterate cfg | "congruence" ->if !Options.disjunction then CongDisjIterator.iterate cfg else CongIterator.iterate cfg | "product" -> if !Options.disjunction then RPDisjIterator.iterate cfg else RPIterator.iterate cfg + | "karr" -> if !Options.disjunction then KarrDisjIterator.iterate cfg else KarrIterator.iterate cfg | _ -> failwith "No valid iterator specified" in Format.printf "@[Failed asserts :@ %a@]" pp_asserts f end diff --git a/examples/karr/karr.c b/examples/karr/karr.c new file mode 100644 index 0000000..5b6b7ac --- /dev/null +++ b/examples/karr/karr.c @@ -0,0 +1,5 @@ +void main() { + int x = rand(0,10); + int y = 3*x; + assert(y == 3*x); +} diff --git a/iterator/iterator.ml b/iterator/iterator.ml index 42ee594..6462699 100644 --- a/iterator/iterator.ml +++ b/iterator/iterator.ml @@ -80,6 +80,7 @@ open Naked open Value_domain open Congruence open Reduced_product +open Karr module IntervalxCongr : CROSS_REDUCTION = struct module V = AddTopBot(Interval) @@ -113,10 +114,11 @@ module SignIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Signs)))) module IntervalIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Interval)))) module CongIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Congruence)))) module RPIterator = Iterator(SimpleIterable(NonRelational(ReducedProduct(IntervalxCongr)))) +module KarrIterator = Iterator(SimpleIterable(Karr)) module ConstDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Constants)))) module SignDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Signs)))) module IntervalDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Interval)))) module CongDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Congruence)))) module RPDisjIterator = Iterator(DisjunctiveIterable(NonRelational(ReducedProduct(IntervalxCongr)))) - +module KarrDisjIterator = Iterator(DisjunctiveIterable(Karr)) diff --git a/scripts/test.sh b/scripts/test.sh index 61909de..4db2dd1 100755 --- a/scripts/test.sh +++ b/scripts/test.sh @@ -272,6 +272,7 @@ treat_examples "interval_loop" "Interval loops" "--domain interval" "" treat_examples "sign" "Sign and misc." "--domain signs" "" treat_examples "congruence" "Congruence operations" "--domain congruence" "" treat_examples "disjunction" "Disjunctive analysis" "--domain congruence" "" +treat_examples "karr" "Karr's domain" "--domain karr" "" echo "" >> $index_html echo "" >> $index_html echo "" >> $index_html