Skip to content

GitLab

Commits (36)
Hide whitespace changes
Inline Side-by-side
bin/frama-c-script
View file @ 5d253f1d
......@@ -38,10 +38,6 @@ usage() {
echo " Interactively prepares a template for analyses,"
echo " writing it to dir/GNUmakefile [default: .frama-c]."
echo ""
echo " - make-path [dir]"
echo " [for Frama-C developers and advanced users without Frama-C in the path]"
echo " Creates a path.mk file in dir [default: .frama-c]."
echo ""
echo " - list-files [path/to/compile_commands.json]"
echo " Lists all sources in the given compile_commands.json"
echo " [default: ./compile_commands.json]."
......@@ -123,34 +119,6 @@ open_file() {
esac
}
make_path() {
dir=".frama-c"
if [ "$#" -gt 0 ]; then
dir="$1"
fi
if [ ! -d "$dir" ]; then
read -p "Directory '$dir' does not exist. Create it? [y/N] " yn
case $yn in
[Yy])
mkdir -p "$dir"
;;
*)
echo "Exiting without creating."
exit 0;;
esac
fi
cat <<EOF > "${dir}/path.mk"
FRAMAC_BIN=${DIR}
ifeq (\$(wildcard \$(FRAMAC_BIN)),)
# Frama-C not installed locally; using the version in the PATH
else
FRAMAC=\$(FRAMAC_BIN)/frama-c
FRAMAC_GUI=\$(FRAMAC_BIN)/frama-c-gui
endif
EOF
echo "Wrote to: ${dir}/path.mk"
}
flamegraph() {
if [ "$#" -eq 0 ]; then
echo "error: 'flamegraph' command requires a path";
......@@ -219,10 +187,6 @@ case "$command" in
shift;
${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@";
;;
"make-path")
shift;
make_path "$@";
;;
"list-files")
shift;
${FRAMAC_SHARE}/analysis-scripts/list_files.py "$@";
......
doc/developer/advance.tex
View file @ 5d253f1d
......@@ -494,12 +494,10 @@ Section~\ref{tut2:hello}). Each variable set in this example has to be set
by any plug-in.
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\makefileinput{./tutorial/hello/generated/makefile_multiple/Makefile}
\texttt{FRAMAC\_SHARE} must be set to the \framac share directory while
\texttt{FRAMAC\_LIBDIR} must be set to the \framac lib directory.
\texttt{FRAMAC\_SHARE} must be set to the \framac share directory.
\texttt{PLUGIN\_NAME} is the capitalized name of your plug-in while
\texttt{PLUGIN\_CMO} is the list of the files $.cmo$ generated from your \caml
sources.
......@@ -596,18 +594,19 @@ otherwise.
\codeidx{clean-install}
\codeidx{install}
In addition, if a plug-in wishes to install custom files to
\texttt{FRAMAC\_LIBDIR} through the \texttt{install::} target,
this target must depend on \texttt{clean-install}.
Indeed, \framac's main \texttt{Makefile} removes
all existing files in this directory before performing a fresh installation,
in order to avoid potential interference with an obsolete (and usually
incompatible) module from a previous installation. Adding the dependency thus
ensures that the removal will take place before any new file has been installed
in the directory.
\begin{example} If a plug-in wants to install \texttt{external/my\_lib.cm*}
in addition to the normal plugin files, it should use the following code:
In addition, if a plug-in wishes to install custom files through the
\texttt{install::} target, this target must depend on \texttt{clean-install}.
Indeed, \framac's main \texttt{Makefile} needs to remove all existing files
before performing a fresh installation, in order to avoid potential interference
with an obsolete (and usually incompatible) module from a previous installation.
Adding the dependency thus ensures that the removal will take place before any
new file has been installed.
\begin{example} If a plug-in wants to install \texttt{external/my\_lib.cm*} in
addition to the normal plugin files, it should use the following code:
\footnote{Note that the variable \texttt{FRAMAC\_LIBDIR} is automatically set
in the \framac \texttt{Makefile} to the value provided by the command
\texttt{frama-c-config -print-libpath}.\codeidx{FRAMAC\_LIBDIR}}
\begin{makefilecode}
install:: clean-install
$(PRINT_INSTALL) "My beautiful library"
......
doc/developer/hello_world/Makefile
View file @ 5d253f1d
......@@ -18,7 +18,6 @@
# before any use of this makefile
FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_world
include $(FRAMAC_SHARE)/Makefile.dynamic
doc/developer/tutorial.tex
View file @ 5d253f1d
......@@ -409,7 +409,6 @@ We write a simple \texttt{./Makefile} for our
\listingname{./Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\makefileinput{./tutorial/hello/generated/makefile_single/Makefile}
......@@ -447,9 +446,9 @@ compiled files are copied into a \texttt{top} (for {\em top-level}) subdirectory
The module can then be loaded and executed by using
\texttt{frama-c -load-module top/Hello}.
Then run \texttt{make install} to install the plug-in (you need to
have write access to the \texttt{\$(FRAMAC\_LIBDIR)/plugins}
directory\codeidx{FRAMAC\_LIBDIR}).
Then run \texttt{make install} to install the plug-in (you need to have write
access to the \texttt{plugins} directory, located at the path given by the
command \texttt{frama-c-config -print-libpath}).
Just launch \texttt{frama-c} (without any option): the \texttt{Hello}
plug-in is now always loaded, without the need to pass other options to
......@@ -467,7 +466,6 @@ file names, in the correct \ocaml build order.
\listingname{./Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\makefileinput{./tutorial/hello/generated/makefile_multiple/Makefile}
......@@ -517,7 +515,6 @@ subdirectory of \texttt{.tests/} where the plug-in's tests will be located:
\listingname{./Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_NAME}
\codeidx{PLUGIN\_TESTS\_DIRS}
......@@ -1073,7 +1070,6 @@ configuration options.
\listingname{Makefile}
\codeidx{Makefile.dynamic}
\codeidx{FRAMAC\_SHARE}
\codeidx{FRAMAC\_LIBDIR}
\codeidx{PLUGIN\_CMO}
\codeidx{PLUGIN\_GUI\_CMO}
\codeidx{PLUGIN\_NAME}
......
doc/developer/tutorial/hello/src/Makefile.multiple-files
View file @ 5d253f1d
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_options hello_print hello_run
include $(FRAMAC_SHARE)/Makefile.dynamic
doc/developer/tutorial/hello/src/Makefile.single-file
View file @ 5d253f1d
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_world
include $(FRAMAC_SHARE)/Makefile.dynamic
doc/developer/tutorial/hello/src/Makefile.test
View file @ 5d253f1d
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = Hello
PLUGIN_CMO = hello_options hello_print hello_run
PLUGIN_TESTS_DIRS := hello
......
doc/developer/tutorial/viewcfg/src/Makefile.split
View file @ 5d253f1d
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
PLUGIN_NAME = ViewCfg
PLUGIN_CMO = cfg_options cfg_core cfg_register
PLUGIN_GUI_CMO = cfg_gui
......
doc/userman/user-analysis-scripts.tex
View file @ 5d253f1d
......@@ -409,9 +409,6 @@ Other commands, only useful in a few cases, are described below.
system, removing optional code features that could prevent \FramaC from
parsing the sources. Currently, it still depends partially on the host system,
so many features are not disabled.
\item[make-path] (for \FramaC developers): to be used when Frama-C is not
installed in the PATH; adds a \texttt{path.mk} file that is used
by the Makefile generated via \texttt{make-template}.
\item[flamegraph]: opens a {\em flamegraph}\footnote{%
See \url{https://github.com/brendangregg/FlameGraph} for details about
flamegraphs.} to visualize which functions take most of the time
......
headers/header_spec.txt
View file @ 5d253f1d
......@@ -1629,6 +1629,8 @@ src/plugins/wp/TacFilter.ml: CEA_WP
src/plugins/wp/TacFilter.mli: CEA_WP
src/plugins/wp/TacHavoc.ml: CEA_WP
src/plugins/wp/TacHavoc.mli: CEA_WP
src/plugins/wp/TacInduction.ml: CEA_WP
src/plugins/wp/TacInduction.mli: CEA_WP
src/plugins/wp/TacInstance.ml: CEA_WP
src/plugins/wp/TacInstance.mli: CEA_WP
src/plugins/wp/TacLemma.ml: CEA_WP
......@@ -1641,6 +1643,8 @@ src/plugins/wp/TacRange.ml: CEA_WP
src/plugins/wp/TacRange.mli: CEA_WP
src/plugins/wp/TacRewrite.ml: CEA_WP
src/plugins/wp/TacRewrite.mli: CEA_WP
src/plugins/wp/TacSequence.ml: CEA_WP
src/plugins/wp/TacSequence.mli: CEA_WP
src/plugins/wp/TacShift.ml: CEA_WP
src/plugins/wp/TacShift.mli: CEA_WP
src/plugins/wp/TacSplit.ml: CEA_WP
......
share/analysis-scripts/make_template.py
View file @ 5d253f1d
......@@ -45,15 +45,10 @@ if len(sys.argv) > 2:
print(" creates a Frama-C makefile in [dir] (default: .frama-c)")
sys.exit(1)
# Note: if Frama-C is in the path, ignore the one in FRAMAC_BIN
framac = shutil.which("frama-c")
if framac:
framac_bin = Path(os.path.dirname(os.path.abspath(framac)))
else:
framac_bin = os.getenv('FRAMAC_BIN')
if not framac_bin:
sys.exit("error: FRAMAC_BIN not in environment")
framac_bin = Path(framac_bin)
framac_bin = os.getenv('FRAMAC_BIN')
if not framac_bin:
sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
framac_bin = Path(framac_bin)
jcdb = Path("compile_commands.json")
......@@ -77,7 +72,7 @@ process = Popen([framac_bin / "frama-c", "-print-config-json"], stdout=PIPE)
(output, err) = process.communicate()
exit_code = process.wait()
if exit_code != 0:
sys.exit(f"error running frama-c -print-share-path")
sys.exit(f"error running frama-c -print-config-json")
fc_config = json.loads(output.decode('utf-8'))
sharedir = Path(fc_config['datadir'])
......@@ -237,13 +232,24 @@ gnumakefile.write_text("".join(lines))
print(f"Template created: {gnumakefile}")
if not "PTESTS_TESTING" in os.environ and not framac:
print(f"Frama-C not in path, adding path.mk to {dir}")
frama_c_script = framac_bin / "frama-c-script"
os.system(f"{frama_c_script} make-path {dir}")
# write path.mk
path_mk = dir / "path.mk"
with open(path_mk, "w") as f:
f.write(f"""FRAMAC_BIN={framac_bin}
ifeq ($(wildcard $(FRAMAC_BIN)),)
# Frama-C not installed locally; using the version in the PATH
else
FRAMAC=$(FRAMAC_BIN)/frama-c
FRAMAC_GUI=$(FRAMAC_BIN)/frama-c-gui
endif
""")
print(f"Path to Frama-C binaries written to: {path_mk}")
if "PTESTS_TESTING" in os.environ:
print("Running ptests: cleaning up after tests...")
jcdb.unlink()
fc_stubs_c.unlink()
path_mk.unlink()
# gnumakefile is not erased because we want it as an oracle
share/analysis-scripts/make_wrapper.py
View file @ 5d253f1d
......@@ -49,7 +49,7 @@ args = args[1:]
framac_bin = os.getenv('FRAMAC_BIN')
if not framac_bin:
sys.exit("error: FRAMAC_BIN not in environment")
sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
framac_script = f"{framac_bin}/frama-c-script"
out = subprocess.Popen(['make', "-C", make_dir] + args,
......
src/kernel_internals/typing/cabs2cil.ml
View file @ 5d253f1d
......@@ -5385,8 +5385,14 @@ and makeCompType ghost (isstruct: bool)
(* Create the self cell for use in fields and forward references. Or maybe
* one exists already from a forward reference *)
let comp, _ = createCompInfo isstruct n' norig in
let doFieldGroup ~is_first_group ~is_last_group ((s: A.spec_elem list),
(nl: (A.name * A.expression option) list)) =
let rec fold f acc = function
| [] -> acc
| [x] -> f ~last:true acc x
| x :: l -> fold f (f ~last:false acc x) l
in
let addFieldGroup ~last:last_group (flds : fieldinfo list)
((s: A.spec_elem list), (nl: (A.name * A.expression option) list)) =
(* Do the specifiers exactly once *)
let sugg = match nl with
| [] -> ""
......@@ -5394,13 +5400,13 @@ and makeCompType ghost (isstruct: bool)
in
let bt, sto, inl, attrs = doSpecList ghost sugg s in
(* Do the fields *)
let makeFieldInfo ~is_first_field ~is_last_field
let addFieldInfo ~last:last_field (flds : fieldinfo list)
(((n,ndt,a,cloc) : A.name), (widtho : A.expression option))
: fieldinfo =
: fieldinfo list =
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true "Storage or inline not allowed for fields";
let allowZeroSizeArrays = true in
let ftype, nattr =
let ftype, fattr =
doType
~allowZeroSizeArrays ghost false (AttrName false) bt
(A.PARENTYPE(attrs, ndt, a))
......@@ -5420,11 +5426,11 @@ and makeCompType ghost (isstruct: bool)
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
then begin
match Cil.unrollType ftype with
| TArray(_,None,_,_) when is_last_field ->
| TArray(_,None,_,_) when last_group && last_field ->
begin
(* possible flexible array member; check if struct contains at least
one other field *)
if is_first_field then (* struct is empty *)
if flds = [] then (* struct is empty *)
Kernel.error ~current:true
"flexible array member '%s' (type %a) \
not allowed in otherwise empty struct"
......@@ -5436,7 +5442,7 @@ and makeCompType ghost (isstruct: bool)
"field `%s' is declared with incomplete type %a"
n Cil_printer.pp_typ ftype
end;
let width, ftype =
let fbitfield, ftype =
match widtho with
| None -> None, ftype
| Some w -> begin
......@@ -5459,9 +5465,14 @@ and makeCompType ghost (isstruct: bool)
w, ftype
end
in
(* Compute the order of the field in the structure *)
let forder = match flds with
| [] -> 0
| { forder=previous_order } :: _ -> previous_order + 1
in
(* If the field is unnamed and its type is a structure of union type
* then give it a distinguished name *)
let n' =
let fname =
if n = missingFieldName then begin
match unrollType ftype with
| TComp _ -> begin
......@@ -5493,52 +5504,34 @@ and makeCompType ghost (isstruct: bool)
| _ -> ()
in
is_circular ftype;
{ fcomp = comp;
{ fcomp = comp;
forder;
forig_name = n;
fname = n';
ftype = ftype;
fbitfield = width;
fattr = nattr;
floc = convLoc cloc;
faddrof = false;
fname;
ftype;
fbitfield;
fattr;
floc = convLoc cloc;
faddrof = false;
fsize_in_bits = None;
foffset_in_bits = None;
fpadding_in_bits = None;
}
in
let rec map_but_last l =
match l with
| [] -> []
| [f] ->
[makeFieldInfo ~is_first_field:false ~is_last_field:is_last_group f]
| f::l ->
let fi = makeFieldInfo ~is_first_field:false ~is_last_field:false f in
[fi] @ map_but_last l
} :: flds
in
match nl with
| [] -> []
| [f] ->
[makeFieldInfo ~is_first_field:is_first_group ~is_last_field:is_last_group f]
| f::l ->
let fi =
makeFieldInfo ~is_first_field:is_first_group ~is_last_field:false f
in
[fi] @ map_but_last l
fold addFieldInfo flds nl
in
(* Do regular fields first. *)
let flds =
List.filter (function FIELD _ -> true | TYPE_ANNOT _ -> false) nglist in
let flds =
List.map (function FIELD (f,g) -> (f,g) | _ -> assert false) flds in
let last = List.length flds - 1 in
let doField i = doFieldGroup ~is_first_group:(i=0) ~is_last_group:(i=last) in
let flds = List.concat (List.mapi doField flds) in
let fld_table = Cil_datatype.Fieldinfo.Hashtbl.create 17 in
let to_field = function
| TYPE_ANNOT _ -> None
| FIELD (f,g) -> Some (f,g) in
let flds = Extlib.filter_map_opt to_field nglist in
let flds = List.rev (fold addFieldGroup [] flds) in
let fld_table = Hashtbl.create 17 in
let check f =
try
let oldf = Cil_datatype.Fieldinfo.Hashtbl.find fld_table f in
let oldf = Hashtbl.find fld_table f.fname in
let source = fst f.floc in
Kernel.error ~source
"field %s occurs multiple times in aggregate %a. \
......@@ -5547,7 +5540,7 @@ and makeCompType ghost (isstruct: bool)
(fst oldf.floc).Filepath.pos_lnum
with Not_found ->
(* Do not add unnamed bitfields: they can share the empty name. *)
if f.fname <> "" then Cil_datatype.Fieldinfo.Hashtbl.add fld_table f f
if f.fname <> "" then Hashtbl.add fld_table f.fname f
in
List.iter check flds;
if comp.cfields <> [] then begin
......
src/kernel_internals/typing/mergecil.ml
View file @ 5d253f1d
......@@ -1151,7 +1151,7 @@ and equalModuloPackedAlign attrs1 attrs2 =
Raises [Failure] if the fields are not equivalent.
If [mustCheckOffsets] is true, then there is already a difference in the
composite type, so each field must be checked. *)
and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets typ_ci1 typ_ci2 f1 f2 =
and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f1 f2 =
if f1.fbitfield <> f2.fbitfield then
raise (Failure "different bitfield info");
if mustCheckOffsets || not (equal_attributes_for_merge f1.fattr f2.fattr) then
......@@ -1160,11 +1160,8 @@ and checkFieldsEqualModuloPackedAlign ~mustCheckOffsets typ_ci1 typ_ci2 f1 f2 =
in which case the difference may be safely ignored *)
begin
try
let offs1, width1 =
Cil.bitsOffset typ_ci1 (Field (f1, NoOffset))
in
let offs2, width2 =
Cil.bitsOffset typ_ci2 (Field (f2, NoOffset))
let offs1, width1 = Cil.fieldBitsOffset f1
and offs2, width2 = Cil.fieldBitsOffset f2
in
if not (equalModuloPackedAlign f1.fattr f2.fattr)
|| offs1 <> offs2 || width1 <> width2 then
......@@ -1252,12 +1249,9 @@ and matchCompInfo (oldfidx: int) (oldci: compinfo)
[%a] vs [%a]"
pp_attrs attrs pp_attrs oldattrs))
in
let typ_ci = TComp(ci, {scache = Not_Computed}, []) in
let typ_oldci = TComp(oldci, {scache = Not_Computed}, []) in
List.iter2
(fun oldf f ->
checkFieldsEqualModuloPackedAlign ~mustCheckOffsets
typ_ci typ_oldci f oldf;
checkFieldsEqualModuloPackedAlign ~mustCheckOffsets f oldf;
(* Make sure the types are compatible *)
(* Note: 6.2.7 §1 states that the names of the fields should be the
same. We do not force this for now, but could do it. *)
......
src/kernel_services/analysis/bit_utils.ml
View file @ 5d253f1d
......@@ -248,8 +248,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
try
let full_fields_to_print = List.fold_left
(fun acc field ->
let current_offset = Field (field,NoOffset) in
let start_o,width_o = bitsOffset typ current_offset in
let start_o,width_o = fieldBitsOffset field in
let start_o,width_o =
Integer.of_int start_o, Integer.of_int width_o
in
......
src/kernel_services/ast_data/cil_types.mli
View file @ 5d253f1d
......@@ -400,6 +400,9 @@ and fieldinfo = {
(** The host structure that contains this field. There can be only one
[compinfo] that contains the field. *)
mutable forder: int;
(** The position in the host structure. *)
forig_name: string;
(** original name as found in C file. *)
......@@ -433,13 +436,14 @@ and fieldinfo = {
expression. *)
mutable fsize_in_bits: int option;
(** (Deprecated. Use {!Cil.bitsOffset} instead.) Similar to [fbitfield] for
all types of fields.
@deprecated only Jessie uses this *)
(** Similar to [fbitfield] for all types of fields.
Do not read this field directly. Use {!Cil.fieldBitsOffset} or
{!Cil.bitsOffset} instead. *)
mutable foffset_in_bits: int option;
(** Offset at which the field starts in the structure. Do not read directly,
but use {!Cil.bitsOffset} instead. *)
(** Offset at which the field starts in the structure.
Do not read this field directly. Use {!Cil.fieldBitsOffset} or
{!Cil.bitsOffset} instead. *)
mutable fpadding_in_bits: int option;
(** (Deprecated.) Store the size of the padding that follows the field, if any.
......
src/kernel_services/ast_printing/cil_printer.ml
View file @ 5d253f1d
......@@ -1833,10 +1833,11 @@ class cil_printer () = object (self)
self#attributes fi.fattr;
if Kernel.(is_debug_key_enabled dkey_print_field_offsets) then
try
let (offset, size) = Cil.bitsOffset fi.ftype (Field (fi, NoOffset)) in
let (offset, size) = Cil.fieldBitsOffset fi in
let first = offset in
let last = offset + size - 1 in
fprintf fmt " /* bits %d .. %d */" first last
let last = if size > 0 then Some (offset + size - 1) else None in
let pp_opt fmt = Pretty_utils.pp_opt ~none:"" Format.pp_print_int fmt in
fprintf fmt " /* bits %d .. %a */" first pp_opt last
with Cil.SizeOfError _ -> ()
method private opt_funspec fmt funspec =
......
src/kernel_services/ast_queries/cil.ml
View file @ 5d253f1d
......@@ -4419,6 +4419,30 @@ and sizeOf ~loc t =
integer ~loc ((bitsSizeOf t) lsr 3)
with SizeOfError _ -> new_exp ~loc (SizeOf(t))
and fieldBitsOffset (f : fieldinfo) : int * int =
if not f.fcomp.cstruct (* union *) then
(* All union fields start at offset 0 *)
0, bitsSizeOf f.ftype
else begin
if f.foffset_in_bits = None then begin
let aux ~last acc fi =
let acc' = offsetOfFieldAcc ~last ~fi ~sofar:acc in
fi.fsize_in_bits <- Some acc'.oaLastFieldWidth;
fi.foffset_in_bits <- Some acc'.oaLastFieldStart;
acc'
in
ignore (
fold_struct_fields aux
{ oaFirstFree = 0;
oaLastFieldStart = 0;
oaLastFieldWidth = 0;
oaPrevBitPack = None }
f.fcomp.cfields
);
end;
Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
end
and bitsOffset (baset: typ) (off: offset) : int * int =
let rec loopOff (baset: typ) (width: int) (start: int) = function
NoOffset -> start, width
......@@ -4432,38 +4456,12 @@ and bitsOffset (baset: typ) (off: offset) : int * int =
let bitsbt = bitsSizeOf bt in
loopOff bt bitsbt (start + ei * bitsbt) off
end
| Field(f, off) when not f.fcomp.cstruct (* union *) ->
| Field(f, off) ->
if check_invariants then
assert (match unrollType baset with
| TComp (ci, _, _) -> ci == f.fcomp
| _ -> false);
(* All union fields start at offset 0 *)
loopOff f.ftype (bitsSizeOf f.ftype) start off
| Field(f, off) (* struct *) ->
if check_invariants then
assert (match unrollType baset with
| TComp (ci, _, _) -> ci == f.fcomp
| _ -> false);
if f.foffset_in_bits = None then begin
let aux ~last acc fi =
let acc' = offsetOfFieldAcc ~last ~fi ~sofar:acc in
fi.fsize_in_bits <- Some acc'.oaLastFieldWidth;
fi.foffset_in_bits <- Some acc'.oaLastFieldStart;
acc'
in
ignore (
fold_struct_fields aux
{ oaFirstFree = 0;
oaLastFieldStart = 0;
oaLastFieldWidth = 0;
oaPrevBitPack = None }
f.fcomp.cfields
);
end;
let offsbits, size =
Extlib.the f.foffset_in_bits, Extlib.the f.fsize_in_bits
in
(match unrollType baset with
| TComp (ci, _, _) -> assert (ci == f.fcomp)
| _ -> assert false);
let offsbits, size = fieldBitsOffset f in
loopOff f.ftype size (start + offsbits) off
in
loopOff baset (bitsSizeOf baset) 0 off
......
src/kernel_services/ast_queries/cil.mli
View file @ 5d253f1d
......@@ -2185,6 +2185,13 @@ val intOfAttrparam: attrparam -> int option
* this after you call {!Cil.initCIL}. *)
val bitsOffset: typ -> offset -> int * int
(** Give a field, returns the number of bits from the structure or union
* containing the field and the width (also expressed in bits) for the subobject
* denoted by the field. Raises {!Cil.SizeOfError} when it cannot compute
* the size. This function is architecture dependent, so you should only call
* this after you call {!Cil.initCIL}. *)
val fieldBitsOffset: fieldinfo -> int * int
(** Like map but try not to make a copy of the list *)
val mapNoCopy: ('a -> 'a) -> 'a list -> 'a list
......
src/kernel_services/ast_queries/cil_const.ml
View file @ 5d253f1d
......@@ -117,8 +117,9 @@ let mkCompInfo
cdefined = false; }
in
let flds =
List.map (fun (fn, ft, fb, fa, fl) ->
List.mapi (fun forder (fn, ft, fb, fa, fl) ->
{ fcomp = comp;
forder;
ftype = ft;
forig_name = fn;
fname = fn;
......