Commit 20b6522b authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'fix/syntax-headers-indent' into 'master'

Fix: Lint + Syntax + Headers

See merge request frama-c/meta!68
parents 499452ba 037501d4
0afa88bd187747a37442be10c916f819cc20dacf
##########################################################################
# #
# This file is part of the Frama-C's MetACSL plug-in. #
# #
# Copyright (C) 2018-2022 #
# 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) #
# #
##########################################################################
#################
# Header config #
#################
| "header_config.txt" -> frame open:"#" line:"#" close:"#"
#############
# CONFIGURE #
#############
| ".*configure\..*" -> frame open:"#" line:"#" close:"#"
##########
# PROLOG #
##########
| ".*\.pl" -> frame open: "%" line: "%" close: "%"
| ".*\.pl" -> skip match: "#!.*"
| ".*\.pl" -> skip match: ":- encoding.*"
| ".*\.pl" -> skip multiline_match: "#!.*" multiline_match: ":- encoding.*"
| ".*\.slog" -> frame open: "%" line: "%" close: "%"
......@@ -167,17 +167,17 @@ let get_callsites_ips kf rips =
do not set up a proxy over a vacuous set of properties. *)
| [] -> []
| _ ->
let segmented =
List.map
(fun rip ->
Statuses_by_call.setup_precondition_proxy kf rip;
List.map
(fun (_, stmt) ->
let segmented =
List.map
(fun rip ->
Statuses_by_call.setup_precondition_proxy kf rip;
List.map
(fun (_, stmt) ->
Statuses_by_call.precondition_at_call kf rip stmt)
calls)
rips
in
List.concat segmented
calls)
rips
in
List.concat segmented
(* Simply modifies a function contract to ensures that pred is a weak invariant *)
class weak_inv_visitor flags full_table table (pre, post) = object (self)
......@@ -320,8 +320,8 @@ let inspect_contract process stmt ckf args =
match b.b_assigns with
| WritesAny ->
Self.warning "Cannot analyze footprint of function %a: no assigns \
clause. Assuming meta-properties with reading/writing contexts are \
valid in this function." Kernel_function.pretty ckf
clause. Assuming meta-properties with reading/writing contexts are \
valid in this function." Kernel_function.pretty ckf
| Writes l -> process ckf stmt vis l ass
) ckf
......@@ -417,17 +417,17 @@ class reading_visitor flags all_mp table = object (self)
in_exp <- true ;
match e.enode with
| SizeOfE _ | AlignOfE _ ->
(* we're not evaluating the expression itself, merely its type. *)
in_exp <- false; Cil.SkipChildren
(* we're not evaluating the expression itself, merely its type. *)
in_exp <- false; Cil.SkipChildren
| AddrOf (_,o) | StartOf(_,o) ->
(* the toplevel lval is not read. However, we might read some lvals
when evaluating the offset. The host is always a Var in this
context, thus we don't need to visit it further. *)
ignore (Visitor.visitFramacOffset (self:>Visitor.frama_c_visitor) o);
in_exp <- false;
Cil.SkipChildren
(* the toplevel lval is not read. However, we might read some lvals
when evaluating the offset. The host is always a Var in this
context, thus we don't need to visit it further. *)
ignore (Visitor.visitFramacOffset (self:>Visitor.frama_c_visitor) o);
in_exp <- false;
Cil.SkipChildren
| _ ->
Cil.DoChildrenPost (fun e -> in_exp <- false ; e)
Cil.DoChildrenPost (fun e -> in_exp <- false ; e)
(* When encoutering an lval in an expression, add it to the statement set *)
method! vlval lval =
......
......@@ -150,10 +150,10 @@ let add_ghost_code flags =
let rec aux = function
| [] -> []
| s :: t ->
let aux_stmt = find_hash_list Stmt_Hashtbl.find_opt to_add s in
if aux_stmt <> [] then
mark_changed (Option.get self#current_func);
aux_stmt @ [s] @ (aux t)
let aux_stmt = find_hash_list Stmt_Hashtbl.find_opt to_add s in
if aux_stmt <> [] then
mark_changed (Option.get self#current_func);
aux_stmt @ [s] @ (aux t)
in block.bstmts <- aux block.bstmts;
block
)
......
......@@ -34,7 +34,7 @@ let emitter = Emitter.create "Deduction engine"
(** ==== PRINTERS FOR THE GENERATION OF PROLOG MODELS ==== *)
(** Print variables as their name and unique id *)
let pp_vi fmt vi =
let pp_vi fmt vi =
Format.fprintf fmt "%s_%d" (String.lowercase_ascii vi.vname) vi.vid
(** Handle offset when printing variables *)
......@@ -86,7 +86,7 @@ let get_vi_name func acc =
(** Expand set formula defining the targets of an HILARE.
In particular, resolve \ALL, \callers, \callees, \in_file
and perform set operations
and perform set operations
*)
let rec compute_target = function
| TgAll ->
......@@ -145,14 +145,14 @@ let generate_callgraph fmt targets =
(** Generic printer for lists *)
let print_setlist pp =
let open Format in
let pp_sep fmt () = pp_print_string fmt ", " in
pp_print_list ~pp_sep pp
let open Format in
let pp_sep fmt () = pp_print_string fmt ", " in
pp_print_list ~pp_sep pp
(** Generic printer for sets of strings *)
let print_set pp fmt s =
StrSet.fold (fun x l -> x :: l) s []
|> print_setlist pp fmt
StrSet.fold (fun x l -> x :: l) s []
|> print_setlist pp fmt
(** In order to get the predicate of an HILARE, we must type it.
......@@ -199,7 +199,7 @@ let identify_pred mp preds globals =
incr predicate_counter;
let fp = compute_footprint unpacked globals in
let print fmt () =
Format.fprintf fmt "property({%a},%s)"
Format.fprintf fmt "property({%a},%s)"
(print_setlist pp_vi) fp
pname
in
......@@ -228,7 +228,7 @@ let is_not_written_predicate globals mp =
| Pseparated [d; l] when Logic_utils.is_same_term d dt ->
begin match l.term_node with
| TAddrOf tlval ->
get_global_variable globals tlval
get_global_variable globals tlval
| _ -> None
end
| _ -> None
......@@ -257,21 +257,21 @@ let is_negative_assigns_predicate globals mp =
(** Export a predicate, trying to match against known patterns *)
let pp_property preds globals mp =
let default () =
let print, preds = identify_pred mp preds globals in
print, preds
let print, preds = identify_pred mp preds globals in
print, preds
in
begin match mp.mp_context with
| Postcond ->
begin match is_negative_assigns_predicate globals mp with
| Some vi_off ->
(fun fmt () ->
Format.fprintf fmt "negative_assigns(%a)" pp_vi_off vi_off), preds
(fun fmt () ->
Format.fprintf fmt "negative_assigns(%a)" pp_vi_off vi_off), preds
| None -> default ()
end
| Writing ->
begin match is_not_written_predicate globals mp with
| Some vi_off ->
(fun fmt () -> Format.fprintf fmt "not_written(%a)" pp_vi_off vi_off), preds
| Some vi_off ->
(fun fmt () -> Format.fprintf fmt "not_written(%a)" pp_vi_off vi_off), preds
| None -> default ()
end
| _ -> default ()
......@@ -279,22 +279,22 @@ let pp_property preds globals mp =
(** Export a whole HILARE: context (as a string), predicate, target set *)
let generate_mp prefix preds globals fmt (mp, tset) =
let print, preds = pp_property preds globals mp in
Format.fprintf fmt "%% Export of HILARE %s@.meta_%s(\"%s\", %a, {%a}).@."
let print, preds = pp_property preds globals mp in
Format.fprintf fmt "%% Export of HILARE %s@.meta_%s(\"%s\", %a, {%a}).@."
mp.mp_name prefix
(match mp.mp_context with
| Weak_invariant -> "Weak invariant"
| Strong_invariant -> "Strong invariant"
| Conditional_invariant -> "Conditional invariant"
| Postcond -> "Postcond"
| Precond -> "Precond"
| Writing -> "Writing"
| Reading -> "Reading"
| Calling -> "Calling"
| Weak_invariant -> "Weak invariant"
| Strong_invariant -> "Strong invariant"
| Conditional_invariant -> "Conditional invariant"
| Postcond -> "Postcond"
| Precond -> "Precond"
| Writing -> "Writing"
| Reading -> "Reading"
| Calling -> "Calling"
)
print ()
(print_set pp_ta) tset;
preds
preds
(** Export all previous HILARE *)
let all_preds = ref None
......@@ -303,7 +303,7 @@ let generate_mps fmt (mps, globals, tsets) =
| [] -> all_preds := Some preds
| mp :: t ->
let preds = generate_mp "ground" preds globals fmt (mp,
(List.assoc mp.mp_name tsets))
(List.assoc mp.mp_name tsets))
in aux preds t
in aux [] mps
......@@ -339,10 +339,10 @@ let deduce flags mp ip mps =
in
let print_goal fmt () =
match !all_preds with
match !all_preds with
| Some p ->
ignore (generate_mp "valid" p globals fmt
(mp, compute_target mp.mp_target))
ignore (generate_mp "valid" p globals fmt
(mp, compute_target mp.mp_target))
| None -> failwith "Oh no"
in
......@@ -377,7 +377,7 @@ go :- %a
close_out oc;
(* Locate where the Prolog model is and go to it *)
let sharedir = Format.asprintf "%a"
Filepath.Normalized.pp_abs (Self.Share.get_dir ".") in
Filepath.Normalized.pp_abs (Self.Share.get_dir ".") in
Sys.chdir sharedir;
(* Run the Prolog model on our file, with a 30s timeout *)
let command = Format.asprintf "./run.pl prove %s 30 > /dev/null" filename in
......
......@@ -91,7 +91,7 @@ let unpack_mp flags mp admit =
{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
* 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
*
......
......@@ -36,7 +36,7 @@ type unpacked_metaproperty = {
val dispatch : meta_flags ->
metaproperty list ->
(context * string list Str_Hashtbl.t) list *
(context * string list Str_Hashtbl.t) list *
(string, unpacked_metaproperty) Hashtbl.t
val name_mp_pred : meta_flags ->
......
......@@ -140,7 +140,7 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
Logic_const.tat (e_t, label)
| PLapp ("\\formal", _, [{lexpr_node = PLvar param}]) ->
let formals = Kernel_function.get_formals kf in
begin try
begin try
let vi = List.find (fun vi -> vi.vname = param) formals in
let lv = Cil.cvar_to_lvar vi in
Logic_const.tvar lv
......@@ -168,7 +168,7 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
begin match List.assoc_opt vname termassoc with
| Some RepVariable a -> a
| None -> meta_ctxt.error loc
"Variable %s forbidden in this context" vname
"Variable %s forbidden in this context" vname
| _ -> meta_ctxt.error loc
"%s expects one argument but has been provided with none" vname
end
......
......@@ -36,7 +36,7 @@ let is_not_orig_variable lv =
| None -> true
(*
* Returns true if two tlvals are obviously \separated
* Returns true if two tlvals are obviously \separated
* That is, if they are both named variables with different names or with non-overlapping
* offsets
*)
......@@ -68,12 +68,12 @@ let neq_lval tl1 tl2 =
match (h1, h2) with
| TVar lv, _ when is_not_orig_variable lv -> true
| _, TVar lv when is_not_orig_variable lv -> true
| TVar l1, TVar l2 ->
| TVar l1, TVar l2 ->
not (Logic_utils.is_same_var l1 l2) || offset_neq of1 of2
| _ -> false
(*
Assuming t is a term representing an address,
(*
Assuming t is a term representing an address,
returns the lval it is an address of
*)
let get_addressed_lval t = match t.term_node with
......@@ -90,7 +90,7 @@ let get_addressed_var_opt t = match t.term_node with
| TStartOf l -> Some l
| _ -> None
(*
(*
* Simplifies \separated predicates to \true or \false when possible, and
* propagates through common logic operators. Also simplifies equality and
* difference when terms are the same
......
......@@ -35,4 +35,3 @@ let find_hash_list find_opt table key =
let add_to_hash_list (find_opt, replace) table key v =
let old_list = find_hash_list find_opt table key in
replace table key (v :: old_list)
(**************************************************************************)
(* *)
(* This file is part of the Frama-C's MetACSL plug-in. *)
(* *)
(* Copyright (C) 2018-2022 *)
(* 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) *)
(* *)
(**************************************************************************)
module Meta_Base
use set.Fset as S
use fmap.Fmap as M
......@@ -123,7 +145,7 @@ module Meta_Lemmas
forall prog: program.
valid_program prog ->
forall fn: function_name. exists f. M.mapsto fn f prog
lemma all_calls_valid_choose:
forall prog, f: function_name.
valid_program prog ->
......
......@@ -41,7 +41,7 @@ reaches(X, Y, A) :-
% 1-step callees of functions in S
callees(S, Callees) :-
Callees = {To :
exists(From,
exists(From,
From in S &
calls(From, To)
)
......@@ -102,13 +102,13 @@ propag_check(_, _, "Strong invariant").
% ------------------
% Avoid long matching time using double negation
fast_meta_ground(C, P, S) :-
fast_meta_ground(C, P, S) :-
var(S) &
meta_ground(C, P, S).
fast_meta_ground(C, P, S) :-
fast_meta_ground(C, P, S) :-
nonvar(S) &
meta_ground(C, P, D) &
meta_ground(C, P, D) &
naf (S neq D).
% -------------------
......
This diff is collapsed.
......@@ -28,18 +28,18 @@ filter_on.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%% equivalence rules
%%%%%%%%%%%%%%%%%%%%%%%% equivalence rules
% equiv_rule(A,B), with A, B {log} predicates: if the input goal contains B then
% equiv_rule(A,B), with A, B {log} predicates: if the input goal contains B then
% then B matches with both filtering rules for A and filtering rules for B (since B => A)
:- op(700,xfx,[ein,enin]).
equiv_rule(e2,inters(X,Y,Z),dinters(X,Y,Z)). % e2. dinters(X,Y,Z) => inters(X,Y,Z)
equiv_rule(e3,ssubset(X,Y),dssubset(X,Y)). % e3. dssubset(X,Y) => ssubset(X,Y)
equiv_rule(e4,nsubset(X,Y),dnsubset(X,Y)). % e4. dnsubset(X,Y) => nsubset(X,Y)
equiv_rule(e5,X in Y,X ein Y). % e5. X ein Y => X in Y
equiv_rule(e6,X nin Y,X enin Y). % e6. X enin Y => X nin Y
equiv_rule(e2,inters(X,Y,Z),dinters(X,Y,Z)). % e2. dinters(X,Y,Z) => inters(X,Y,Z)
equiv_rule(e3,ssubset(X,Y),dssubset(X,Y)). % e3. dssubset(X,Y) => ssubset(X,Y)
equiv_rule(e4,nsubset(X,Y),dnsubset(X,Y)). % e4. dnsubset(X,Y) => nsubset(X,Y)
equiv_rule(e5,X in Y,X ein Y). % e5. X ein Y => X in Y
equiv_rule(e6,X nin Y,X enin Y). % e6. X enin Y => X nin Y
%TO BE COMPLETED: esubset, einters, ...
......@@ -53,7 +53,7 @@ equiv_rule(e6,X nin Y,X enin Y). % e6. X enin Y => X nin Y
% D: list of other atomic constraints to be checked
% D_Conds: list of conditions for atomic constraints in D and C
% AddC: constraint to be replaced to C)
%%%%% general
% t = X -replace-> X = t
......@@ -64,27 +64,27 @@ replace_rule(br3,T=X,[var(X),nonvar(T)],[],[],X=T).
% inters(X,{...},t3) -replace-> inters({...},X,t3)
replace_rule(r3,inters(X,T2,T3),[var(X),nonvar(T2)],[],[],inters(T2,X,T3)).
% A neq B & set(A) & set(B) -replace-> (X in A & X nin B or X nin A & X in B)
% A neq B & set(A) & set(B) -replace-> (X in A & X nin B or X nin A & X in B)
replace_rule(r4,A neq B,[var(A),var(B)],[set(A1),set(B1)],[A1==A,B1==B],(X in A & X nin B or X nin A & X in B)).
% A neq {...} & set(A) -replace-> (X in A & X nin {...} or X nin A & X in {...})
% A neq {...} & set(A) -replace-> (X in A & X nin {...} or X nin A & X in {...})
replace_rule(r4,A neq B,[var(A),nonvar(B),B=_ with _],[set(A1)],[A1==A],(X in A & X nin B or X nin A & X in B)).
% {...} neq B & set(B) -replace-> (X in B & X nin {...} or X nin B & X in {...})
% {...} neq B & set(B) -replace-> (X in B & X nin {...} or X nin B & X in {...})
replace_rule(r4,A neq B,[var(B),nonvar(A),A=_ with _],[set(B1)],[B1==B],(X in A & X nin B or X nin A & X in B)).
%%%%% relations/partial functions
%%%%% relations/partial functions
% dom(Rel,Dom) & pfun(Rel) -replace-> dompf(Rel,Dom) & pfun(Rel)
% dom(Rel,Dom) & pfun(Rel) -replace-> dompf(Rel,Dom) & pfun(Rel)
replace_rule(br4,dom(Rel,Dom),[var(Rel)],[pfun(Rel1)],[Rel1==Rel],dompf(Rel,Dom)).
% comp(R,S,Q) & pfun(R) & pfun(S) -replace-> comppf(R,S,Q) & pfun(Q) & pfun(R) & pfun(S)
replace_rule(br5,comp(R,S,Q),[var(R),var(S)],[pfun(R1),pfun(S1)],[R1==R,S1==S],comppf(R,S,Q) & pfun(Q)).
% dres(A,R,S) & pfun(R) -replace-> drespf(A,R,S) & pfun(R)
% dres(A,R,S) & pfun(R) -replace-> drespf(A,R,S) & pfun(R)
replace_rule(br6,dres(A,R,S),[var(R)],[pfun(R1)],[R1==R],drespf(A,R,S)).
% rel(R) & pfun(R) -replace-> pfun(R) & pfun(R)
% rel(R) & pfun(R) -replace-> pfun(R) & pfun(R)
replace_rule(br7,rel(R),[var(R)],[pfun(R1)],[R1==R],pfun(R)).
%un(S,T,cp(A,A)) -replace-> delay(un(S,T,cp(A,A)),false)
......@@ -120,7 +120,7 @@ replace_rule(br2,X =< Y,[var(X),var(Y)],[],[],Y >= X).
% D_Conds: list of conditions for atomic constraints in D and C
% E: list of constraints in D to be NOT checked
% AddC: constraint to be added)
%%%%% sets
%inters(X,Y,Z) & un(X,Y,Z) -+-> X = Y & Y = Z
......@@ -145,7 +145,7 @@ inference_rule('length-length',length(L,N),[var(L)],[length(L1,M)],[L1==L],[leng
% X > Y & Y > Z -add-> X > Z
inference_rule('gt-gt',X > Y,[var(X),var(Y)],[Y1 > Z],[Y1==Y,Z\==X],[X > Y], X > Z).
% X >= Y & Y >= X -add-> X = Y
inference_rule('ge-ge',X >= Y,[var(X),var(Y)],[Y1 >= X1],[Y1==Y,X1==X],[], X = Y).
......@@ -172,16 +172,16 @@ inference_rule('sum-sum',X is Y + K,[var(X),var(Y),integer(K)],[Z is Y1 + K1],[v
fail_rule('gt-gt',X > Y,[],[V > W],[V==Y,W==X],[]).
% it works also for X > X
% bf2. X >= Y & Y > X
% bf2. X >= Y & Y > X
fail_rule('ge-gt',X >= Y,[],[V > W],[V==Y,W==X],[]).
%%%%% sets
% bf3. X in S & X nin S
% bf3. X in S & X nin S
fail_rule('in-nin',X in S,[var(S)],[X1 nin S1],[X1==X,S1==S],[]).
% bf4. NotSubsetOfSingleton
% A neq {} & ssubset(A,{X})
% A neq {} & ssubset(A,{X})
fail_rule('NotSubsetOfSingleton',ssubset(A,S),[nonvar(S),S={} with _X],[A1 neq E],[nonvar(E),E={},A1==A],[]).
%%%%% intervals (terminating, provided all variables have "not too big" domains)
......@@ -191,7 +191,7 @@ fail_rule('NotSubsetOfSingleton',ssubset(A,S),[nonvar(S),S={} with _X],[A1 neq E
fail_rule('NatRangeNotEmpty',I=int(X,Y),[var(X),var(Y)],[X1 is Expr1,Y1 is Expr2,I1=E],[nonvar(Expr1),Expr1=(Z+A),integer(A),nonvar(Expr2),Expr2=(Z1+B),integer(B),A=<B,nonvar(E),E={},X1==X,Y1==Y,Z1==Z,I1==I],[]).
% f21. NatRangeNotEq3
% I=int(X,Y) & J=int(a,b) & I=J & X is Z+N & Y is Z+M & N is V*h & M =< P & P is W*h & W is V+k
% I=int(X,Y) & J=int(a,b) & I=J & X is Z+N & Y is Z+M & N is V*h & M =< P & P is W*h & W is V+k
% and a,b,h,k integer constants >= 0 and it holds that b-a > k*h
%
fail_rule('NatRangeNotEq3',I=int(X,Y),
......@@ -219,7 +219,7 @@ fail_rule('NatRangeNotSubset',I=int(X,Y),
I==I1,J==J1,X==X1,Y==Y1,N==N1,M==M1,Za=Za1,Zb==Zb1,Zc==Zc1],[]).
% f23. NatRangeNotEq
% I=int(X,Y) & J=int(Kn,Km) & I=J & X is N+Za & Y is N+Zb & Za is M*Kp & Zb is Zc*Kp & Zc is M+Kq
% I=int(X,Y) & J=int(Kn,Km) & I=J & X is N+Za & Y is N+Zb & Za is M*Kp & Zb is Zc*Kp & Zc is M+Kq
% with Km-Kn > Kq*Kp
%
fail_rule('NatRangeNotEq',I=int(X,Y),
......@@ -260,9 +260,9 @@ fail_rule('NatRangeNotEmpty4',I=int(N,Y),
% Add here other more specific user-defined rewriting rules
%%%%%%%%%%%%%%%%%%%%%%%% for the TTF
:- (exists_file('TTF_rules.pl'),!,consult('TTF_rules.pl')
;
:- (exists_file('TTF_rules.pl'),!,consult('TTF_rules.pl')
;
true).
Supports Markdown
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