convert.mli

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -22,7 +22,23 @@
 
 open Intermediate_format
 
+(** attribute decorating member functions that are implicitly defined
+    by Frama-Clang. *)
+val fc_implicit_attr: string
+
+(** attribute decorating templated member functions that are never defined
+    (i.e. fully instantiated). Their presence in the AST tends to be
+    dependent on the clang version used for type-checking.
+*)
+val fc_pure_template_decl_attr: string
+
 (** creates the name of the field corresponding to a direct base class. *)
 val create_base_field_name: Convert_env.env -> qualified_name -> tkind -> string
- 
+
 val convert_ast: Intermediate_format.file -> Cabs.file
+
+(** remove unneeded definitions and declarations. Notably:
+    - unused implicit definitions
+    - templated member functions that are not defined and never used.
+*)
+val remove_unneeded: Cil_types.file -> unit

convert_acsl.mli

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -24,11 +24,14 @@
 
 val convert_function_contract:
   Convert_env.env ->
-  Intermediate_format.function_contract -> Logic_ptree.spec
+  Intermediate_format.function_contract ->
+  Convert_env.env * Logic_ptree.spec
 
 val convert_code_annot:
   Convert_env.env ->
-  Intermediate_format.code_annotation -> Logic_ptree.code_annot
+  Intermediate_format.code_annotation ->
+  Convert_env.env * Logic_ptree.code_annot
 
 val convert_annot:
-  Convert_env.env -> Intermediate_format.global_annotation -> Logic_ptree.decl
+  Convert_env.env -> Intermediate_format.global_annotation ->
+  Convert_env.env * Logic_ptree.decl

convert_env.ml

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -45,6 +45,7 @@ type env =
     local_vars: typ Datatype.String.Map.t;
     captured_vars: bool Datatype.String.Map.t list;
     global_vars: (bool * typ) Fclang_datatype.Qualified_name.Map.t;
+    functions: (bool * typ) Fclang_datatype.Qualified_name.Map.t;
     is_extern_c: bool;
     is_ghost: bool;
     current_func_name: qualified_name;
@@ -78,6 +79,7 @@ let empty_env =
     local_vars = Datatype.String.Map.empty;
     captured_vars = [];
     global_vars = Fclang_datatype.Qualified_name.Map.empty;
+    functions = Fclang_datatype.Qualified_name.Map.empty;
     is_extern_c = false;
     is_ghost = false;
     current_func_name = empty_func_name;
@@ -160,7 +162,7 @@ let temp_name env s =
 
 let set_loc env loc =
   let loc = Cil_datatype.Location.of_lexing_loc loc in
-  Cil.CurrentLoc.set loc; { env with location = loc }
+  { env with location = loc }
 
 let get_loc env = env.location
 
@@ -230,13 +232,27 @@ let set_current_func_name env name =
   set_class_from_qual env name
 
 let reset_func env =
+  let functions =
+    Fclang_datatype.Qualified_name.Map.add
+      (env.current_func_name, TStandard)
+      (env.is_extern_c, env.current_return_type)
+      env.functions
+  in
   let new_env =
     { env with
+      functions;
       current_func_name = empty_func_name;
       current_return_type = empty_return_type }
   in
   reset_class_from_qual new_env env.current_func_name
 
+let get_func env name =
+  try
+    Fclang_datatype.Qualified_name.Map.find (name, TStandard) env.functions
+  with Not_found ->
+    fatal env "Unknown function %a"
+      Fclang_datatype.Qualified_name.pretty (name, TStandard)
+
 let get_current_func_name env = env.current_func_name.decl_name
 
 let set_current_return_type env typ =
@@ -258,6 +274,24 @@ let get_typedef env name =
 let has_typedef env name =
   Fclang_datatype.Qualified_name.Map.mem (name, TStandard) env.typedefs
 
+let memo_wchar env =
+  let wchar_name = { prequalification=[];decl_name="wchar_t"} in
+  if has_typedef env wchar_name then env
+  else begin
+    let kind = Machine.wchar_kind () in
+    let repr = Cxx_utils.(unqual_type (int_type kind)) in
+    let env = add_typedef env wchar_name repr in
+    let ghost = is_ghost env in
+    let env = set_ghost env false in
+    let loc = get_loc env in
+    let spec = Cxx_utils.spec_of_ikind kind in
+    let name = ["wchar_t", Cabs.JUSTBASE, [], loc] in
+    let def = Cabs.TYPEDEF((spec,name),loc) in
+    let env = add_c_global env def in
+    let env = set_ghost env ghost in
+    env
+  end
+
 let rec template_parameter_normalize env tparam = match tparam with
   | TPStructOrClass name -> TPStructOrClass
     { name with prequalification
@@ -763,9 +797,6 @@ and get_dynamic_signature env e =
       let signature = get_dynamic_signature env ptr.econtent in
       get_signature_type env signature.result.plain_type
     | Temporary(_, ctyp, _, _) -> get_signature_type env ctyp.plain_type
-    | LambdaExpr(result, args, _, _) ->
-      let parameter = List.map (fun x -> x.arg_type) args in
-      { result; parameter; variadic = false }
     | _ -> fatal env "no function type information for expression"
 
 let add_closure_info env capture =
@@ -793,3 +824,12 @@ let reset_closure env =
   match env.captured_vars with
   | [] -> env
   | _::captured_vars -> { env with captured_vars }
+
+let env_map f env l =
+  let do_one (env, acc) x = let env, y = f env x in env,y::acc in
+  let env, res = List.fold_left do_one (env,[]) l in
+  env, List.rev res
+
+let env_opt f env = function
+  | Some x -> let env, y = f env x in env, Some y
+  | None -> env, None

convert_env.mli

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -113,6 +113,8 @@ val get_current_return_type: env -> typ
 val reset_func: env -> env
 (** also reset the namespace if needed *)
 
+val get_func: env -> qualified_name -> (bool * typ)
+
 val get_current_class: env -> Fclang_datatype.Qualified_name.t option
 
 val set_current_class: env -> Fclang_datatype.Qualified_name.t -> env
@@ -128,6 +130,11 @@ val get_typedef: env -> qualified_name -> qual_type
 
 val has_typedef: env -> qualified_name -> bool
 
+val memo_wchar: env -> env
+(** adds a definition of wchar_t if not already present. Used when encountering
+    [wchar_t] on the C++ side.
+*)
+
 val add_struct: env -> (qualified_name * tkind) -> (string * qual_type) list
     -> env
 
@@ -315,3 +322,13 @@ val reset_closure: env -> env
 
 val add_closure_info: env -> capture list -> env
   (** Associates the given identifiers to the appropriate closure kind. *)
+
+(** iterates a function that might change the environment over a list,
+    and returns the final environment together with the list of results
+*)
+val env_map: (env -> 'a -> (env * 'b)) -> env -> 'a list -> (env * 'b list)
+
+(** [env_opt f env opt] applies [f] if [opt] has a value, and [None], without
+    changing the environment otherwise.
+*)
+val env_opt: (env -> 'a -> (env * 'b)) -> env -> 'a option -> (env * 'b option)

convert_link.ml

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -29,9 +29,9 @@ let transform_category =
 let exn_dkey = Frama_Clang_option.register_category "exn:inherit"
 
 let find_comp name =
-  try 
+  try
     (match Globals.Types.find_type Logic_typing.Struct name with
-      | TComp(c,_,_) -> c
+      | { tnode = TComp c } -> c
       | _ ->
         Frama_Clang_option.fatal "unexpected type returned for struct %s" name)
   with Not_found ->
@@ -44,7 +44,7 @@ let rec coerce lv comp path =
     | (_,_,direct_base) :: path ->
       let cname = Extlib.uncurry Mangling.mangle direct_base None in
       let fname =
-        Extlib.uncurry 
+        Extlib.uncurry
           (Convert.create_base_field_name Convert_env.empty_env) direct_base
       in
       let field = Cil.getCompField comp fname in
@@ -57,8 +57,8 @@ let add_subtypes kf = function
   | Catch_all -> Catch_all
   | Catch_exn(vi,l) as bind ->
     let loc = vi.vdecl in
-    (match (Cil.unrollType vi.vtype) with
-      | TComp({ corig_name = base },_,_) as base_struct ->
+    (match Ast_types.unroll vi.vtype with
+      | { tnode = TComp { corig_name = base } } as base_struct ->
         let qualified_base = Class.class_of_mangled base in
         (match qualified_base with
           | Some qualified_base ->
@@ -101,7 +101,7 @@ let add_subtypes kf = function
                     Cil.makeTempVar f
                       ~insert:false
                       ~name:(vi.vname ^ "_" ^ (string_of_int i))
-                      (TComp (struct_info, { scache = Not_Computed }, []))
+                      (Cil_const.mk_tcomp struct_info)
                   in
                   f.slocals <- my_vi :: f.slocals;
                   let lv = coerce (Cil.var my_vi) struct_info path in
@@ -113,7 +113,7 @@ let add_subtypes kf = function
                 end else acc
               in
               let _,binders =
-                Fclang_datatype.Qualified_name.Set.fold 
+                Fclang_datatype.Qualified_name.Set.fold
                   treat_one_derived derived (1,binders)
               in
               Catch_exn(vi,binders)
@@ -131,7 +131,7 @@ class clean =
           let c =
             List.map
               (fun (bind, body) ->
-                add_subtypes (Extlib.the self#current_kf) bind, body)
+                add_subtypes (Option.get self#current_kf) bind, body)
               c
           in
           s.skind <- TryCatch(t,c,l);

convert_link.mli

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)

cxx_utils.ml

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -393,6 +393,23 @@ let meth_name class_name tkind decl_name =
   let prequalification= List.append class_name.prequalification [last_elt] in
   { prequalification; decl_name }
 
+let int_kind = function
+  | Cil_types.IBool -> IBool
+  | IChar ->
+    if Machine.char_is_unsigned () then IChar_u else IChar_s
+  | IUChar -> IUChar
+  | ISChar -> ISChar
+  | IInt -> IInt
+  | IUInt -> IUInt
+  | IShort -> IShort
+  | IUShort -> IUShort
+  | ILong -> ILong
+  | IULong -> IULong
+  | ILongLong -> ILongLong
+  | IULongLong -> IULongLong
+
+let int_type ikind = Intermediate_format.Int (int_kind ikind)
+
 let unqual_type t = { qualifier = []; plain_type = t }
 
 let const_type t = { qualifier = [ Const ]; plain_type = t }
@@ -408,10 +425,6 @@ let force_ptr_to_const p =
     { p with plain_type = Pointer (PDataPointer t) }
   | _ -> p
 
-let make_lambda_type result args closure =
-  let parameter = List.map (fun x -> x.arg_type) args in
-  Lambda ({ result; parameter; variadic = false }, closure)
-
 let plain_obj_ptr t = Pointer (PDataPointer t)
 
 let plain_obj_lvref t = LVReference (PDataPointer t)
@@ -435,3 +448,20 @@ let class_ptr (n,t) = unqual_type (plain_class_ptr (n,t))
 let class_lvref (n,t) = unqual_type (plain_class_lvref (n,t))
 
 let class_rvref (n,t) = unqual_type (plain_class_rvref (n,t))
+
+let spec_of_ikind s =
+  let open Cabs in
+  let open Cil_types in
+  match s with
+  | IBool -> [ SpecType Tbool ]
+  | IChar -> [ SpecType Tchar ]
+  | ISChar -> [ SpecType Tsigned; SpecType Tchar ]
+  | IUChar -> [ SpecType Tunsigned; SpecType Tchar ]
+  | IInt -> [ SpecType Tint ]
+  | IUInt -> [ SpecType Tunsigned ]
+  | IShort -> [ SpecType Tshort ]
+  | IUShort -> [ SpecType Tunsigned; SpecType Tshort ]
+  | ILong -> [ SpecType Tlong ]
+  | IULong -> [ SpecType Tunsigned; SpecType Tlong ]
+  | ILongLong -> [ SpecType Tlong; SpecType Tlong ]
+  | IULongLong -> [ SpecType Tunsigned; SpecType Tlong; SpecType Tlong ]

cxx_utils.mli

@@ -2,7 +2,7 @@
 (*                                                                        *)
 (*  This file is part of Frama-Clang                                      *)
 (*                                                                        *)
-(*  Copyright (C) 2012-2020                                               *)
+(*  Copyright (C) 2012-2025                                               *)
 (*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
 (*         alternatives)                                                  *)
 (*                                                                        *)
@@ -59,6 +59,9 @@ val meth_name: qualified_name -> tkind -> string -> qualified_name
 
 (** {3 Types}. *)
 
+(** returns an IR typ corresponding to the Cil's kind *)
+val int_type: Cil_types.ikind -> typ
+
 (** returns the unqualified version of the given typ. *)
 val unqual_type: typ -> qual_type
 
@@ -73,9 +76,6 @@ val const_qual_type: qual_type -> qual_type
  *)
 val force_ptr_to_const: qual_type -> qual_type
 
-(** creates a lambda type with the given signature and captured ids. *)
-val make_lambda_type: qual_type -> arg_decl list -> capture list -> typ
-
 (** given an object type, returns an unqualified pointer type to the object. *)
 val obj_ptr: qual_type -> qual_type
 
@@ -102,3 +102,5 @@ val class_ptr: Fclang_datatype.Qualified_name.t -> qual_type
 val class_lvref: Fclang_datatype.Qualified_name.t -> qual_type
 
 val class_rvref: Fclang_datatype.Qualified_name.t -> qual_type
+
+val spec_of_ikind: Cil_types.ikind -> Cabs.specifier

doc/support/MakeLaTeXModern

-FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf
-
-frama-c-book.cls: ../frama-c-book.cls
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"
-
-frama-c-cover.pdf: ../frama-c-cover.pdf
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"
-
-frama-c-right.pdf: ../frama-c-right.pdf
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"
-
-frama-c-left.pdf: ../frama-c-left.pdf
-	@rm -f $@
-	@cp $< .
-	@chmod a-w $@
-	@echo "import $<"

doc/userman/CLANG_VERSION

+11.0-18.0

doc/userman/FCLANG_VERSION

+0.0.17+dev

doc/userman/FC_VERSION

+30.0+dev

doc/userman/FC_VERSION_NAME

+Zinc

doc/userman/Makefile

 MAIN=main
 
-C_CODE=$(wildcard examples/*.[ci])
-FC_VERSION+=Potassium+
-
 DEPS_MODERN=biblio.bib \
-	changes.tex \
-    description.tex \
-	grammar.tex \
-	introduction.tex \
-	limitations.tex \
-	macros.tex \
-	preprocessing.tex \
-	fclangversion.tex \
-	$(C_CODE) \
-	Makefile
+ changes.tex \
+ description.tex \
+ grammar.tex \
+ introduction.tex \
+ limitations.tex \
+ macros.tex \
+ preprocessing.tex \
+ fclangversion.tex \
 
 default: main.pdf
 
 main.pdf: main.tex $(DEPS_MODERN)
 
 FCLANG_DIR=../..
-DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
+
 install:
 	mkdir -p $(FCLANG_DIR)/doc/manuals/
 	cp -f main.pdf $(FCLANG_DIR)/doc/manuals/fclang-manual.pdf
 
-include $(FCLANG_DIR)/doc/support/MakeLaTeXModern
-
-version.tex: Makefile
-
-%.1: %.mp
-	mpost -interaction=batchmode $<
-
-%.mps: %.1
-	mv $< $@
-
-%.pp: %.tex pp
-	./pp -utf8 $< > $@
-
-%.pp: %.c pp
-	./pp -utf8 -c $< > $@
-
-%.tex: %.ctex pp
-	rm -f $@
-	./pp $< > $@
-	chmod a-w $@
-
-%.bnf: %.tex transf
-	rm -f $@
-	./transf $< > $@
-	chmod a-w $@
-
-%_modern.bnf: %.tex transf
-	rm -f $@
-	./transf -modern $< > $@
-	chmod a-w $@
-
-%.ml: %.mll
-	ocamllex $<
-
 %.pdf: %.tex
-	latexmk $<
-
-%.cmo: %.ml
-	ocamlc -c $<
-
-pp: pp.ml
-	ocamlopt -o $@ str.cmxa $^
-
-transf: transf.cmo transfmain.cmo
-	ocamlc -o $@ $^
-
-transfmain.cmo: transf.cmo
+	latexmk -pdf $<
 
-.PHONY: clean
+.PHONY:clean
 
 clean:
-	rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
-		*.haux  *.hbbl *.htoc \
-                *.cb* *.cm? *.bbl *.blg *.idx *.ind *.ilg \
-		transf trans.ml pp.ml pp
+	latexmk -c main

doc/userman/biblio.bib

@@ -158,3 +158,16 @@ Properties}},
   author = {Kostyantyn Vorobyov and Julien Signoles and Nikolai Kosmatov},
   note  = {Submitted for publication},
 }
+
+
+@article{baudinCACM21,
+	title = {The {Dogged} {Pursuit} of {Bug}-{Free} {C} {Programs}: {The} {Frama}-{C} {Software} {Analysis} {Platform}},
+	volume = {64},
+	url = {https://cacm.acm.org/magazines/2021/8},
+	number = {8},
+	journal = {Communications of the ACM},
+	author = {Baudin, Patrick and Bobot, François and Bühler, David and Correnson, Loïc and Kirchner, Florent and Kosmatov, Nikolai and Maroneze, André and Perrelle, Valentin and Prevosto, Virgile and Signoles, Julien and Williams, Nicky},
+	month = aug,
+	year = {2021},
+	pages = {56--68},
+}

doc/userman/changes.tex

 \chapter{Changes}\label{chap:changes}
 
-This chapter summarizes the changes in \fclang and its documentation
+This chapter summarizes the changes in \framaclang and its documentation
 between each release, with the most recent releases first.
 
+\section*{Version 0.0.15}
+\begin{itemize}
+\item
+  Better handling of mixed C/C++ code and \texttt{extern\ "C"}
+  declarations
+\item
+  Compatibility with Clang 17
+\item
+  Compatibility with Frama-C 28.x Nickel
+\end{itemize}
+
+\section*{Version 0.0.14}
+\begin{itemize}
+\item Compatibility with \FramaC 27.x Cobalt.
+\item Compatibility with \clang 15.0 and 16.0. \clang 10.0 is not supported anymore.
+\item \framaclang has an official \opam package.
+\end{itemize}
+
+\section*{Version 0.0.13}
+\begin{itemize}
+\item Compatibility with \FramaC 25.0
+\item added \texttt{limits} and \texttt{ratio} headers (contributed by T-Gruber)
+\end{itemize}
+
+\section*{Version 0.0.12}
+\begin{itemize}
+\item compatibility with \clang 13.0 and \clang 14.0
+\item \clang >= 10 is now required
+\item compatibility with \FramaC 24.0
+\item support for C++14 generic lambdas (contributed by S. Gränitz)
+\item option for printing reparseable code and using demangling also on non-C++ sources
+\end{itemize}
+
+\section*{Version 0.0.11}
+\begin{itemize}
+\item compatibility with \clang 12.0
+\item compatibility with \FramaC 23.0
+\item Slightly improved ACSL++ parsing
+\item Various bug fixes
+\end{itemize}
+
+\section*{Version 0.0.10}
+\begin{itemize}
+\item compatibility with \clang 11.x
+\item compatibility with \FramaC 22.x
+\item don't generate code for implicit member functions and operators when
+ they're not used
+\item don't generate code for templated member functions that are in fact never
+  instantiated
+\end{itemize}
+
 \section*{Version 0.0.9}
 \begin{itemize}
 \item compatibility with \clang 10.0
-\item compatibility with \framac 21.x
+\item compatibility with \FramaC 21.x
 \item support for implicit initialization of POD objects.
 \end{itemize}
 
 \section*{Version 0.0.8}
 \begin{itemize}
 \item compatibility with \clang 9.0
-\item compatibility with \framac 20.0
+\item compatibility with \FramaC 20.0
 \item proper conversion of ghost statements
 \item support for \acslpp \lstinline|\exit_status|
 \item C++-part of the plug-in is now free from g++ warnings