package frama-c-metacsl
MetAcsl plugin of Frama-C for writing pervasives properties
Install
Dune Dependency
Authors
Maintainers
Sources
meta-0.9-beta.tar.bz2
md5=32bd324617144e618a39e0015445effb
sha512=d96bc4fb9e4c9771efeca815aa1d6f2bae0676cce56d9ed227370bacf4fb04c0811d53470cd15981406ae11a0e95af9f16ab31f7cac04ae2a92cbf85233fb496
doc/src/frama-c-metacsl.core/meta_dispatch.ml.html
Source file meta_dispatch.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
(**************************************************************************) (* *) (* This file is part of the Frama-C's MetACSL plug-in. *) (* *) (* Copyright (C) 2018-2025 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file LICENSE) *) (* *) (**************************************************************************) open Cil_types open Meta_utils open Meta_parse open Meta_options type unpacked_metaproperty = { ump_emitter : Emitter.t; ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate; ump_ip : Property.t; ump_counter : int ref; ump_admit : bool; ump_assert : bool; } let name_of_meta_acsl_term t = match t.term_node with | TConst LStr s -> s | _ -> failwith "Invalid meta term" let get_mp_ip mp = let vis = object (_) inherit Visitor.frama_c_inplace val mutable found = None method get () = Option.get found method! vannotation = function | Dextended ({ext_name = "meta"; ext_kind = Ext_terms [t]} as ext, _, _) when name_of_meta_acsl_term t = mp.mp_name -> found <- Some (Property.ip_of_extended Property.ELGlob ext); Cil.SkipChildren | _ -> Cil.DoChildren end in ignore (Visitor.visitFramacFileSameGlobals (vis :> Visitor.frama_c_visitor) (Ast.get ())); vis # get () let name_mp_pred flags pred ump_counter = let pred = if flags.prefix_meta then {pred with pred_name = "meta" :: pred.pred_name} else pred in if flags.number_assertions then ( (* Number the instantiation *) ump_counter := !ump_counter + 1; {pred with pred_name = ("_" ^ (string_of_int !ump_counter)) :: pred.pred_name} ) else pred let unpack_mp flags mp admit = let ump_emitter = Emitter.create mp.mp_name ~correctness:[] ~tuning:[] [Emitter.Code_annot] in let ump_ip = get_mp_ip mp in let ump_counter = ref 0 in (* Wrapped property *) let ump_property kf ?stmt al = let pred = mp.mp_property kf al in let pred = match stmt with | None -> pred | Some stmt -> Meta_simplify.remove_alpha_conflicts pred kf stmt in let pred = if flags.simpl then Meta_simplify.simplify pred else pred in pred in let ump_assert = match mp.mp_translation with | MtNone -> assert false | MtAssert -> true | MtCheck -> false | MtDefault -> flags.default_to_assert in {ump_emitter; ump_property; ump_ip; ump_counter; ump_admit = admit; ump_assert} (* Returns an assoc list associating each context to a * hash table mapping each function to a list of * MP names to process for that context and for that function. * The order is the same as in the original file * * Also returns a hash table mapping a MP name to an unpacked MP *) let dispatch flags mps = let all_mp = Hashtbl.create 10 in let ctxts = [Weak_invariant; Strong_invariant; Writing; Reading; Calling; Precond; Postcond; Conditional_invariant] in let tables = List.map (fun ctx -> ctx, Str_Hashtbl.create 5) ctxts in List.iter (fun mp -> let table = List.assoc mp.mp_context tables in let targets = Meta_deduce.compute_target mp.mp_target in if flags.list_targets then Self.feedback "Targets of %s: %a" mp.mp_name StrSet.pretty targets ; let admit = match mp.mp_proof_method with | MmLocal -> false | MmAxiom -> true | MmDeduction -> let ip = get_mp_ip mp in Meta_deduce.deduce flags mp ip mps in if mp.mp_translation <> MtNone then ( StrSet.iter (fun target -> add_to_hash_list Str_Hashtbl.(find_opt, replace) table target mp.mp_name ) targets; Hashtbl.add all_mp mp.mp_name (unpack_mp flags mp admit) ); ) mps; (* Reverse lists in tables to maintain the correct order *) List.iter (fun (_, table) -> Str_Hashtbl.iter (fun k v -> Str_Hashtbl.replace table k (List.rev v) ) table ) tables; tables, all_mp module UmpHash = struct type t = unpacked_metaproperty let equal a b = Emitter.equal a.ump_emitter b.ump_emitter let hash p = Emitter.hash p.ump_emitter end module UmpHashtbl = Hashtbl.Make(UmpHash) (* Associates a list of deps (IPs) to an UMP *) let dependencies = UmpHashtbl.create 10 (* Call each time an instantiation of a prop is done *) let add_dependency ump ips = List.iter (add_to_hash_list UmpHashtbl.(find_opt, replace) dependencies ump) ips (* Call once at the end to actually register dependencies between props and * their instanciations *) let finalize_dependencies () = let keys = UmpHashtbl.to_seq_keys dependencies in let add_one prop = let deps = find_hash_list UmpHashtbl.find_opt dependencies prop in (* If the MP is admitted, every instance *is* true *) if prop.ump_admit then List.iter (fun inst -> Property_status.emit prop.ump_emitter ~hyps:[] inst Property_status.True ) deps else ( (* The MP is true if every instance is true *) Property_status.emit prop.ump_emitter ~hyps:deps prop.ump_ip Property_status.True ) in Seq.iter add_one keys
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>