Attachment #180847 for bug #245806

Lines 857-862 Link Here

(-)frama-c-Lithium-20081201/Makefile.in (-1 / +2 lines)
857	src/memory_state/memzone_type.cmo \	857	src/memory_state/memzone_type.cmo \
858	src/memory_state/widen_type.cmo \	858	src/memory_state/widen_type.cmo \
859	src/memory_state/relations_type.cmo \	859	src/memory_state/relations_type.cmo \
		860	src/memory_state/state_set.cmo \
860	src/logic/why_output.cmo	861	src/logic/why_output.cmo
861		862
862	ACMX = $(ACMO:.cmo=.cmx)	863	ACMX = $(ACMO:.cmo=.cmx)
Lines 1023-1029 Link Here
1023	PLUGIN_ENABLE:=@ENABLE_VALUE@	1024	PLUGIN_ENABLE:=@ENABLE_VALUE@
1024	PLUGIN_NAME:=Value	1025	PLUGIN_NAME:=Value
1025	PLUGIN_DIR:=src/value	1026	PLUGIN_DIR:=src/value
1026	PLUGIN_CMO:= state_set kf_state eval kinstr register	1027	PLUGIN_CMO:= kf_state eval kinstr register
1027	PLUGIN_GUI_CMO:=register_gui	1028	PLUGIN_GUI_CMO:=register_gui
1028	PLUGIN_HAS_MLI:=yes	1029	PLUGIN_HAS_MLI:=yes
1029	PLUGIN_GUI_HAS_MLI:=yes	1030	PLUGIN_GUI_HAS_MLI:=yes

Lines 257-262 Link Here

(-)frama-c-Lithium-20081201/src/kernel/db.ml (+6 lines)
257	type t = (kernel_function * kinstr) list * state InstrHashtbl.t	257	type t = (kernel_function * kinstr) list * state InstrHashtbl.t
258	end)	258	end)
259		259
		260	module Record_Value_Superposition_Callbacks =
		261	Hook.Build
		262	(struct
		263	type t = (kernel_function * kinstr) list * State_set.t InstrHashtbl.t
		264	end)
		265
260	module Call_Value_Callbacks =	266	module Call_Value_Callbacks =
261	Hook.Build	267	Hook.Build
262	(struct type t = state * (Db_types.kernel_function * kinstr) list end)	268	(struct type t = state * (Db_types.kernel_function * kinstr) list end)

Lines 248-253 Link Here

(-)frama-c-Lithium-20081201/src/kernel/db.mli (+3 lines)
248	module Record_Value_Callbacks:	248	module Record_Value_Callbacks:
249	Hook.S with type param = (kernel_function * kinstr) list	249	Hook.S with type param = (kernel_function * kinstr) list
250	* state Cilutil.InstrHashtbl.t	250	* state Cilutil.InstrHashtbl.t
		251	module Record_Value_Superposition_Callbacks:
		252	Hook.S with type param = (kernel_function * kinstr) list
		253	* State_set.t Cilutil.InstrHashtbl.t
251		254
252	(** Actions to perform at each treatment of a "call" statement.	255	(** Actions to perform at each treatment of a "call" statement.
253	@plugin development guide *)	256	@plugin development guide *)




    (*Format.printf "Done Merging current@.";*)

    if not degenerate &&
      ((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_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

	  current_table;

	Db.Value.Record_Value_Callbacks.apply
	  (stack_for_callbacks, current_states);
         end	  
      end;
    InstrHashtbl.clear current_table;


Return to bug 245806

Lines 2526-2533 Link Here

(-)frama-c-Lithium-20081201/src/value/eval.ml (-2 / +21 lines)
2526	(Format.printf "Done Merging current@.";)	2526	(Format.printf "Done Merging current@.";)
2527		2527
2528	if not degenerate &&	2528	if not degenerate &&
2529	not (Db.Value.Record_Value_Callbacks.is_empty ())	2529	((not (Db.Value.Record_Value_Callbacks.is_empty ())) \|\|
		2530	(not (Db.Value.Record_Value_Superposition_Callbacks.is_empty ())))
2530	then begin	2531	then begin
		2532	let stack_for_callbacks = for_callbacks_stack () in
		2533
		2534	if not (Db.Value.Record_Value_Callbacks.is_empty ())
		2535	then begin
		2536	let current_superpositions = InstrHashtbl.create 17 in
		2537	InstrHashtbl.iter
		2538	(fun k record ->
		2539	InstrHashtbl.add current_superpositions k record.superposition)
		2540	current_table;
		2541
		2542	(* Format.printf "[values] now calling Record_Value_Superposition callbacks@."; *)
		2543	Db.Value.Record_Value_Superposition_Callbacks.apply
		2544	(stack_for_callbacks, current_superpositions);
		2545
		2546	end ;
		2547	if not (Db.Value.Record_Value_Callbacks.is_empty ())
		2548	then begin
2531	(* Format.printf "[values] now calling Record_Value callbacks@."; *)	2549	(* Format.printf "[values] now calling Record_Value callbacks@."; *)
2532		2550
2533	let current_states = InstrHashtbl.create 17 in	2551	let current_states = InstrHashtbl.create 17 in
Lines 2537-2543 Link Here
2537	current_table;	2555	current_table;
2538		2556
2539	Db.Value.Record_Value_Callbacks.apply	2557	Db.Value.Record_Value_Callbacks.apply
2540	((for_callbacks_stack ()), current_states);	2558	(stack_for_callbacks, current_states);
		2559	end
2541	end;	2560	end;
2542	InstrHashtbl.clear current_table;	2561	InstrHashtbl.clear current_table;
2543		2562