Commit bd02d6d2 authored by Sylvain Dailler's avatar Sylvain Dailler

More reliable printing of counterexamples interleaved with source.

Filename problems remain.
parent aeab66d7
......@@ -467,7 +467,6 @@ let interleave_with_source
?(end_comment=" *)")
?(me_name_trans = why_name_trans)
model
~filename
~rel_filename
~source_code
~locations =
......@@ -476,7 +475,15 @@ let interleave_with_source
(List.filter (fun x -> let (f, _, _, _) = Loc.get (fst x) in f = rel_filename) locations)
in
try
let model_file = StringMap.find filename model.model_files in
(* There is no way to compare rel_filename and the locations of filename in
the file because they contain extra ".." which cannot be reliably removed
(because of potential symbolic link). So, we use the basename.
*)
let model_files =
StringMap.filter (fun k _ -> Filename.basename k = Filename.basename rel_filename)
model.model_files
in
let model_file = snd (StringMap.choose model_files) in
let src_lines_up_to_last_cntexmp_el source_code model_file =
let (last_cntexmp_line, _) = IntMap.max_binding model_file in
Str.bounded_split (Str.regexp "^") source_code (last_cntexmp_line+1)
......
......@@ -259,7 +259,6 @@ val interleave_with_source :
?end_comment:string ->
?me_name_trans:(model_element_name -> string) ->
model ->
filename:string ->
rel_filename:string ->
source_code:string ->
locations:(Loc.position * 'a) list ->
......@@ -274,7 +273,6 @@ val interleave_with_source :
@param end_comment the string that ends a comment
@param me_name_trans see print_model
@param model counter-example model
@param filename the file name of the source
@param rel_filename the file name of the source relative to the session
@param source_code the input source code
@param locations the source locations that are found in the code
......
......@@ -901,7 +901,7 @@ end
in
let source_code = Sysutil.file_contents filename in
Model_parser.interleave_with_source ?start_comment:None ?end_comment:None
?me_name_trans:None res.Call_provers.pr_model ~filename:filename ~rel_filename:(file_name f)
?me_name_trans:None res.Call_provers.pr_model ~rel_filename:(file_name f)
~source_code:source_code ~locations:list_loc
let send_task nid show_full_context loc =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment