diff options
Diffstat (limited to 'sci-mathematics/frama-c/files/frama-c-20090601_beta1-states_hook.patch')
| -rw-r--r-- | sci-mathematics/frama-c/files/frama-c-20090601_beta1-states_hook.patch | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/sci-mathematics/frama-c/files/frama-c-20090601_beta1-states_hook.patch b/sci-mathematics/frama-c/files/frama-c-20090601_beta1-states_hook.patch new file mode 100644 index 000000000..ca0630520 --- /dev/null +++ b/sci-mathematics/frama-c/files/frama-c-20090601_beta1-states_hook.patch @@ -0,0 +1,90 @@ +diff -Naur frama-c-Beryllium-20090601-beta1-orig/Makefile.in frama-c-Beryllium-20090601-beta1-ptch/Makefile.in +--- frama-c-Beryllium-20090601-beta1-orig/Makefile.in 2009-06-23 11:24:39.000000000 +0000 ++++ frama-c-Beryllium-20090601-beta1-ptch/Makefile.in 2009-07-12 03:45:51.000000000 +0000 +@@ -661,6 +661,7 @@ + src/memory_state/memzone_type.cmo \ + src/memory_state/widen_type.cmo \ + src/memory_state/relations_type.cmo \ ++ src/memory_state/state_set.cmo \ + src/kernel/stmts_graph.cmo \ + src/kernel/visitor.cmo \ + src/kernel/printer.cmo src/kernel/unroll_loops.cmo \ +@@ -771,7 +772,7 @@ + PLUGIN_ENABLE:=@ENABLE_VALUE@ + PLUGIN_NAME:=Value + PLUGIN_DIR:=src/value +-PLUGIN_CMO:= state_set kf_state value_parameters eval kinstr register ++PLUGIN_CMO:= kf_state value_parameters eval kinstr register + PLUGIN_GUI_CMO:=register_gui + PLUGIN_HAS_MLI:=yes + PLUGIN_NO_TEST:=yes +diff -Naur frama-c-Beryllium-20090601-beta1-orig/src/kernel/db.ml frama-c-Beryllium-20090601-beta1-ptch/src/kernel/db.ml +--- frama-c-Beryllium-20090601-beta1-orig/src/kernel/db.ml 2009-07-12 03:41:32.000000000 +0000 ++++ frama-c-Beryllium-20090601-beta1-ptch/src/kernel/db.ml 2009-07-12 03:42:41.000000000 +0000 +@@ -261,6 +261,12 @@ + type t = (kernel_function * kinstr) list * state InstrHashtbl.t + end) + ++ module Record_Value_Superposition_Callbacks = ++ Hook.Build ++ (struct ++ type t = (kernel_function * kinstr) list * State_set.t InstrHashtbl.t ++ end) ++ + module Call_Value_Callbacks = + Hook.Build + (struct type t = state * (Db_types.kernel_function * kinstr) list end) +diff -Naur frama-c-Beryllium-20090601-beta1-orig/src/kernel/db.mli frama-c-Beryllium-20090601-beta1-ptch/src/kernel/db.mli +--- frama-c-Beryllium-20090601-beta1-orig/src/kernel/db.mli 2009-07-12 03:41:32.000000000 +0000 ++++ frama-c-Beryllium-20090601-beta1-ptch/src/kernel/db.mli 2009-07-12 03:42:41.000000000 +0000 +@@ -282,6 +282,9 @@ + module Record_Value_Callbacks: + Hook.S with type param = (kernel_function * kinstr) list + * state Cilutil.InstrHashtbl.t ++ module Record_Value_Superposition_Callbacks: ++ Hook.S with type param = (kernel_function * kinstr) list ++ * State_set.t Cilutil.InstrHashtbl.t + + (** Actions to perform at each treatment of a "call" statement. + @plugin development guide *) +diff -Naur frama-c-Beryllium-20090601-beta1-orig/src/value/eval.ml frama-c-Beryllium-20090601-beta1-ptch/src/value/eval.ml +--- frama-c-Beryllium-20090601-beta1-orig/src/value/eval.ml 2009-06-23 09:08:08.000000000 +0000 ++++ frama-c-Beryllium-20090601-beta1-ptch/src/value/eval.ml 2009-07-12 03:42:41.000000000 +0000 +@@ -2773,8 +2773,26 @@ + (* Format.printf "Done Merging current@."; *) + + if not degenerate && +- not (Db.Value.Record_Value_Callbacks.is_empty ()) ++ ((not (Db.Value.Record_Value_Callbacks.is_empty ())) || ++ (not (Db.Value.Record_Value_Superposition_Callbacks.is_empty ()))) + then begin ++ let stack_for_callbacks = for_callbacks_stack () in ++ ++ if not (Db.Value.Record_Value_Superposition_Callbacks.is_empty ()) ++ then begin ++ let current_superpositions = InstrHashtbl.create 17 in ++ InstrHashtbl.iter ++ (fun k record -> ++ InstrHashtbl.add current_superpositions k record.superposition) ++ current_table; ++ ++(* Format.printf "[values] now calling Record_Value_Superposition callbacks@."; *) ++ Db.Value.Record_Value_Superposition_Callbacks.apply ++ (stack_for_callbacks, current_superpositions); ++ ++ end ; ++ if not (Db.Value.Record_Value_Callbacks.is_empty ()) ++ then begin + (* Format.printf "[values] now calling Record_Value callbacks@."; *) + + let current_states = InstrHashtbl.create 17 in +@@ -2785,7 +2803,8 @@ + current_table; + + Db.Value.Record_Value_Callbacks.apply +- ((for_callbacks_stack ()), current_states); ++ (stack_for_callbacks, current_states); ++ end + end; + InstrHashtbl.clear current_table; + |