Project

General

Profile

« Previous | Next » 

Revision 4174a469

Added by Guillaume Davy over 9 years ago

Correct some problem related to new bool encoding

View differences:

src/backends/C/c_backend_proof.ml
573 573 
            (pp_acsl_val mem1 (pp_acsl_var_read "" [])) y
574 574 
            mem2 i
575 575 
        | MStep (il, i, vl) ->
576 
          let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "%a" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read "" [])) x in
576 
          let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "%a" | _ -> fprintf fmt "%a") (pp_acsl_val mem1 (pp_acsl_var_read "" pointer)) x in
577 577 
          pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i m.mcalls)))) fmt
578 578 
          ((List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_val_type x)*) pp_val x) vl)@
579 
          (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" []) x) il)@
579 
          (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read "" pointer) x) il)@
580 580 
            (try ignore(List.assoc i m.minstances);[(fun fmt->fprintf fmt "%s.%s" mem1 i);(fun fmt->fprintf fmt "%s.%s" mem2 i)] with Not_found -> []))
581 581 
        | MBranch (g,hl) -> assert false
582 582 
      in
......
585 585 
        | MLocalAssign (i,v) -> [fun fmt -> if List.exists (fun o -> o.var_id = i.var_id) pointer
586 586 
    then fprintf fmt "*%s" i.var_id
587 587 
    else fprintf fmt "%s" i.var_id]
588 
        | MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%a" (pp_acsl_val mem2 (pp_acsl_var_read "" pointer)) (StateVar i)]
588 
        | MStateAssign (i,v) -> [fun fmt -> fprintf fmt "%s._reg.%s" mem2 i.var_id]
589 589 
        | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> [fun fmt -> fprintf fmt "%a" (pp_acsl_var_read "" pointer) i0]
590 590 
        | MStep ([i0], i, [x;y]) when (not (Basic_library.is_internal_fun i)) && (node_name (fst (List.assoc i m.mcalls)) = "_arrow") ->
591 591 
          [fun fmt-> fprintf fmt "%t, %s.%s" (fun fmt -> if List.exists (fun o -> o.var_id = i0.var_id) pointer
......
746 746 
    *)
747 747 

  		




  748
  748
  
    
    let pp_coq_goal name goalname code fmt =


  		




  749
  
  
    
        fprintf fmt "Goal %t.\nProof.\n%aQed.\n\n" (fun fmt-> fprintf fmt goalname name) code name


  		




  
  749
  
    
        fprintf fmt "Goal %t.\nProof.\n%aQed.\n\n" goalname code name


  		




  750
  750
  
    

  		




  751
  751
  
    
    let pp_coq stateless fmt m =


  		




  752
  752
  
    
      match m.mspec with


  		




  753
  753
  
    
        | Some _ ->


  		




  754
  754
  
    
          let name = m.mname.node_id in


  		




  755
  755
  
    
          if name <> arrow_id then (


  		




  756
  
  
    
            pp_coq_goal name "typed_%s_step_post" pp_code_inv fmt;


  		




  757
  
  
    
            pp_coq_goal name "typed_ref_%s_step_post" pp_code_inv fmt;


  		




  758
  
  
    
            pp_coq_goal name "typed_lemma_inv_inv_%s" (pp_code_inv_inv m) fmt


  		




  
  756
  
    
            pp_coq_goal name (fun fmt -> fprintf fmt "typed_%s_step_post" name) pp_code_inv fmt;


  		




  
  757
  
    
            pp_coq_goal name (fun fmt -> fprintf fmt "typed_ref_%s_step_post" name) pp_code_inv fmt;


  		




  
  758
  
    
            pp_coq_goal name (fun fmt -> fprintf fmt "typed_lemma_inv_inv_%s" name) (pp_code_inv_inv m) fmt;


  		




  
  759
  
    
            pp_coq_goal name (fun fmt -> fprintf fmt "typed_ref_lemma_missing") (fun fmt name-> fprintf fmt "admit.\n") fmt


  		




  759
  760
  
    
          )


  		




  760
  761
  
    
        | _ -> ()


  		




  761
  762
  
    

  		












Also available in:  Unified diff