Skip to content
Snippets Groups Projects
Commit 7b13fa19 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'fix/andre/plugins-gitignore' into 'master'

remove obsolete .gitignore files

See merge request frama-c/frama-c!4660
parents 716ccebb b2ede665
No related branches found
No related tags found
No related merge requests found
Showing
with 0 additions and 612 deletions
......@@ -3,24 +3,15 @@
###########
TAGS
*.annot
#ocamlyacc -v
*.output
*~
*_DEP
*.depend
\#*
.\#*
.DS_Store
*.tmp
#artifacts from execution
frama_c_journal.ml
/.frama-c/
/frama-c*.tar.gz
/.merlin
/headers/hdrck
/headers/hdrck.exe
/bin/ivette
.ivette
......@@ -54,19 +45,10 @@ _bisect
/tests/crowbar/mutable
/tests/crowbar/output-*
/tests/crowbar/test_ghost_cfg
/tests/*/*.opt
/.test-errors.log
/dev/fc-time
/dev/fc-memuse
/bin/ocamldep_transitive_closure
#share
/share/Makefile.config
/share/Makefile.dynamic_config
/share/Makefile.kernel
/share/frama-c.rc
#created by create_share_link target
/share/.gitignore
/share/manuals/
......@@ -110,11 +92,6 @@ _bisect
/doc/code/print_api/dynamic_plugins.mli
/doc/code/print_api/_build/
/doc/developer/tutorial/viewcfg/src/META.frama-c-viewcfg
/doc/developer/tutorial/viewcfg/src/Makefile
/doc/developer/tutorial/viewcfg/src/gui/
/doc/developer/tutorial/viewcfg/src/top/
/doc/doxygen
/doc/pdg/call-f.eps
......@@ -144,23 +121,7 @@ _bisect
/doc/server/
#lib
/lib/fc/
/lib/plugins/*.mli
/lib/plugins/*.ml
/lib/plugins/top/
/lib/plugins/gui/
/lib/plugins/top/
/lib/plugins/META.frama-c-*
/lib/plugins/.placeholders_ready
#plugins
/share/e-acsl/
/share/c2fc/
/src/plugins/*/configure
/src/plugins/*/.depend
/src/plugins/*/autom4te.cache/
/src/plugins/*/Makefile.plugin.generated
/src/plugins/*/doc/*/*.dot
/src/plugins/*/doc/*/*.aux
/src/plugins/*/doc/*/*.bbl
......@@ -173,7 +134,6 @@ _bisect
/src/plugins/*/doc/*/*.log
/src/plugins/*/doc/*/*.out
/src/plugins/*/doc/*/*.idx
Makefile.plugin.generated
# WP/Coq Generated file
.lia.cache
......@@ -187,19 +147,6 @@ share/analysis-scripts/fc-estimate-difficulty
share/analysis-scripts/fc-estimate-difficulty.exe
share/analysis-scripts/libc_metrics.json
# generated ML files
/src/libraries/utils/json.ml
/src/kernel_internals/runtime/fc_config.ml
/src/kernel_internals/parsing/logic_lexer.ml
/src/kernel_internals/parsing/logic_parser.ml
/src/kernel_internals/parsing/logic_parser.mli
/src/kernel_internals/parsing/logic_preprocess.ml
/src/kernel_internals/parsing/clexer.ml
/src/kernel_internals/parsing/cparser.ml
/src/kernel_internals/parsing/cparser.mli
/src/plugins/markdown-report/META
# generated tar.gz files
/doc/developer/hello.tar.gz
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2024 *)
(* 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 licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
let depend_files = ref []
let add_deps s = depend_files:= s :: !depend_files
let root = ref ""
module Dep_graph = Graph.Imperative.Digraph.Concrete(
struct
type t = string
let compare = String.compare
let hash = Hashtbl.hash
let equal = (=)
end)
module Dfs = Graph.Traverse.Dfs(Dep_graph)
module Topological = Graph.Topological.Make(Dep_graph)
module String_set = Set.Make(String)
let dependencies = Dep_graph.create ()
let tokenize_input chan =
let rec aux acc =
let line = input_line chan in
let tokens = Str.(split (regexp " +") line) in
match List.rev tokens with
| "\\" :: tail -> aux (tail @ acc)
| l -> l @ acc
in
List.rev (aux [])
let add_edge user provider =
if Filename.check_suffix user ".cmx" &&
Filename.check_suffix provider ".cmx"
then Dep_graph.add_edge dependencies user provider
let parse_one_dependency chan =
match tokenize_input chan with
| [] -> () (* Empty line *)
| target :: ":" :: deps ->
List.iter (add_edge target) deps;
| _ -> failwith ("ill formed rule")
let read_dep_file file =
let chan = open_in file in
try
while true do
parse_one_dependency chan
done;
with End_of_file -> close_in chan
let usage =
Printf.sprintf
"usage: %s -root file.cmx -deps .depend\n\
provides the ordered list of .cmx needed to link file.cmx \
(excluding the latter)"
(Filename.basename Sys.executable_name)
let err_usage () = Printf.printf "%s\n%!" usage; exit 2
let arguments =
[ "-deps", Arg.String add_deps, "add a .depend file to set of dependencies";
"-root", Arg.Set_string root, "root of the dependencies computation";
]
let () =
Arg.parse arguments (fun _ -> err_usage()) usage;
List.iter read_dep_file !depend_files;
let add v acc = if v = !root then acc else String_set.add v acc in
let res = Dfs.fold_component add String_set.empty dependencies !root in
let l =
Topological.fold
(fun s acc -> if String_set.mem s res then s :: acc else acc)
dependencies []
in
Format.(printf "@[<h>%a@]"
(pp_print_list
~pp_sep:(fun fmt () -> pp_print_string fmt " ") pp_print_string)
l)
(**************************************************************************)
(* *)
(* Copyright (C) Jean-Christophe Filliatre *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(*i $Id: size.ml,v 1.1 2007-11-28 12:52:04 uid568 Exp $ i*)
(*i*)
open Obj
(*i*)
(*s Pointers already visited are stored in a hash-table, where
comparisons are done using physical equality. *)
external address_of_value: 'a -> int = "address_of_value"
module H = Hashtbl.Make(
struct
type t = Obj.t
let equal = (==)
let hash = address_of_value
end)
let node_table = (H.create 257 : unit H.t)
let in_table o = try H.find node_table o; true with Not_found -> false
let add_in_table o = H.add node_table o ()
let reset_table () = H.clear node_table
(*s Objects are traversed recursively, as soon as their tags are less than
[no_scan_tag]. [count] records the numbers of words already visited. *)
let size_of_double = size (repr 1.0)
let count = ref 0
let rec traverse t =
if not (in_table t) then begin
add_in_table t;
if is_block t then begin
let n = size t in
let tag = tag t in
if tag < no_scan_tag then begin
count := !count + 1 + n;
for i = 0 to n - 1 do
let f = field t i in
if is_block f then traverse f
done
end else if tag = string_tag then
count := !count + 1 + n
else if tag = double_tag then
count := !count + size_of_double
else if tag = double_array_tag then
count := !count + 1 + size_of_double * n
else
incr count
end
end
(*s Sizes of objects in words and in bytes. The size in bytes is computed
system-independently according to [Sys.word_size]. *)
let res () =
let r = !count in
reset_table ();
r
let size_w ?except o =
reset_table ();
(match except with
| None -> ()
| Some except -> traverse (repr except)
);
count := 0;
traverse (repr o);
res ()
let size_b ?except o = (size_w ?except o) * (Sys.word_size / 8)
let size_kb ?except o = (size_w ?except o) / (8192 / Sys.word_size)
(**************************************************************************)
(* *)
(* Copyright (C) Jean-Christophe Filliatre *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
(* énergies alternatives). *)
(* *)
(**************************************************************************)
(*i $Id: size.mli,v 1.1 2007-11-28 12:52:04 uid568 Exp $ i*)
(* Sizes of ocaml values (in their memory representation).
Sizes are given in words ([size_w]), bytes ([size_b]) or kilobytes
([size_kb]), in a system-independent way. *)
val size_w : ?except:'a -> 'b -> int
val size_b : ?except:'a -> 'b -> int
val size_kb : ?except:'a -> 'b -> int
(**************************************************************************)
(* *)
(* Copyright (C) Jean-Christophe Filliatre *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(* Modified by CEA *)
open Obj
(* Pointers already visited are stored in a hash-table, where
comparisons are done using physical equality. *)
external address_of_value: 'a -> int = "address_of_value"
module H = Hashtbl.Make(
struct
type t = Obj.t
let equal = (==)
let hash = address_of_value
end)
let node_table = (H.create 257 : unit H.t)
(* Addresses that will be skipped *)
let except_table = (H.create 257 : unit H.t)
let in_table o = H.mem node_table o || H.mem except_table o
let add_in_table o = H.add node_table o ()
let mark_as_skipped () =
H.iter (fun addr () -> H.add except_table addr ()) node_table
let reset_table () = H.clear node_table
(*s Objects are traversed recursively, as soon as their tags are less than
[no_scan_tag]. [count] records the numbers of words already visited. *)
let size_of_double = size (repr 1.0)
let count = ref 0
let rec traverse t =
if not (in_table t) then begin
add_in_table t;
if is_block t then begin
let n = size t in
let tag = tag t in
if tag < no_scan_tag then begin
count := !count + 1 + n;
for i = 0 to n - 1 do
let f = field t i in
if is_block f then traverse f
done
end else if tag = string_tag then
count := !count + 1 + n
else if tag = double_tag then
count := !count + size_of_double
else if tag = double_array_tag then
count := !count + 1 + size_of_double * n
else
incr count
end
end
let res () =
let r = !count in
reset_table ();
count := 0;
r
(* CEA *)
let all_sizes () =
Gc.compact ();
Gc.set { (Gc.get ()) with
Gc.max_overhead = 1000000; allocation_policy = 1 } (* disable compaction *);
let states =
State_builder.States.fold (fun name _ v _ acc -> (name, Obj.repr v) :: acc) []
in
let ast = List.assoc "AST" states in
let add acc name =
let size : int = (res ()) / 1000 in
if size <> 0 then (size, name) :: acc else acc
in
(* Compute the size of the AST, and mark the entire AST as skipped *)
traverse ast;
mark_as_skipped ();
let res = add [] "AST" in
(* Now traverse the other states, but implicitly excluding the AST *)
let aux acc (state, v) =
traverse v;
add acc state
in
let res = List.fold_left aux res states in
(* Sort by increasing size *)
let res = List.sort (fun (s1, _) (s2, _) -> compare s1 s2) res in
let pp fmt (size, name) = Format.fprintf fmt "@[%d kW, %s@]" size name in
Kernel.result "## Sizes ##@.%a"
(Pretty_utils.pp_list ~pre:"@[<v>" ~suf:"@]" ~sep:"@ " pp) res
let () = Boot.Main.extend all_sizes
=========================================================================
Ce fichier contient les règles à suivre pour écrire la doc du développeur
=========================================================================
* Les instructions de "doc/www/src/metadoc.NE_PAS_ECRIRE" doivent être
appliquées.
* Les fichiers portent l'extension .pretex pour permettre leur preprocessing
* L'index doit être tenu à jour
* Les redondances dans l'index (deux entrées différentes correspondant à la
même chose) ne sont autorisées seulement si une des deux entrées référence
proprement l'autre à l'aide d'un tag "see".
* L'annexe "Changes" doit être tenue à jour.
* Les macros doivent être définies dans macros.tex
* Les macros doivent être au maximum utilisées.
En particulier:
o les environnements dérivés de "code" pour le code
- autoconfcode pour les configure.in
- makecode pour les makefile
- ccode pour le C
- camlcode pour le caml
- code pour les autres codes (ligne de commandes par exemple)
o l'environnement "example" pour les exemples
o l'environnement "important" pour les choses importantes
o l'environnement "convention" pour les conventions qu'un développeur doit
respecter
o l'environnement "prereq" pour les prérequis nécessaires à la bonne
compréhension
o les macros pour les noms de langage/d'outils (c'est la même macro
\langage à l'origine)
o les macros pour les entrées d'index
Do not add any files in this directory:
It should only be used by Makefile.plugin.
description="frama-c"
version=""
requires=""
package "kernel" (
description="The kernel library of frama-c"
version=""
requires="@REQUIRES"
archive(byte) = "frama-c.cma"
plugin(byte) = "frama-c.cma"
archive(native) = "frama-c.cmxa"
plugin(native) = "frama-c.cmxs"
directory=""
)
directory=""
/**************************************************************************/
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2024 */
/* 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 licenses/LGPLv2.1). */
/* */
/**************************************************************************/
; Script generated by the Inno Setup Script Wizard.
; SEE THE DOCUMENTATION FOR DETAILS ON CREATING INNO SETUP SCRIPT FILES!
#define MyAppName "Frama-C"
#define MyAppVerName "Frama-C Boron 20100401"
#define MyAppPublisher "CEA LIST"
#define MyAppURL "http://frama-c.com"
#define MyAppExeName "frama-c-gui.exe"
[Setup]
; NOTE: The value of AppId uniquely identifies this application.
; Do not use the same AppId value in installers for other applications.
; (To generate a new GUID, click Tools | Generate GUID inside the IDE.)
AppId={{0726456B-CCA1-4836-BEBB-4C5D0DD832E2}
AppName={#MyAppName}
AppVerName={#MyAppVerName}
AppPublisher={#MyAppPublisher}
AppPublisherURL={#MyAppURL}
AppSupportURL={#MyAppURL}
AppUpdatesURL={#MyAppURL}
DefaultDirName=C:\{#MyAppName}
DefaultGroupName={#MyAppName}
AllowNoIcons=yes
OutputBaseFilename=frama-c-Boron-20100401
SetupIconFile=C:\Frama-C\share\frama-c\frama-c.ico
Compression=lzma
SolidCompression=yes
ChangesEnvironment=yes
InfoAfterFile=win32_manual_installation_step.txt
[Languages]
Name: "english"; MessagesFile: "compiler:Default.isl"
[Tasks]
Name: "desktopicon"; Description: "{cm:CreateDesktopIcon}"; GroupDescription: "{cm:AdditionalIcons}"; Flags: unchecked
Name: "quicklaunchicon"; Description: "{cm:CreateQuickLaunchIcon}"; GroupDescription: "{cm:AdditionalIcons}"; Flags: unchecked
[Files]
Source: "C:\Frama-C\bin\frama-c-gui.exe"; DestDir: "{app}\bin"; Flags: ignoreversion
Source: "C:\Frama-C\*"; DestDir: "{app}"; Flags: ignoreversion recursesubdirs createallsubdirs
Source: "C:\DEV_ROOT\GTK\*"; DestDir: "{app}"; Flags: ignoreversion recursesubdirs createallsubdirs
Source: "C:\DEV_ROOT\ocamlmgw\*"; DestDir: "{app}"; Flags: ignoreversion recursesubdirs createallsubdirs
; NOTE: Don't use "Flags: ignoreversion" on any shared system files
[Icons]
Name: "{group}\{#MyAppName}"; Filename: "{app}\bin\{#MyAppExeName}"; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
Name: "{group}\manuals"; Filename: "{app}\share\frama-c\manuals"; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
Name: "{commondesktop}\{#MyAppName}"; Filename: "{app}\bin\{#MyAppExeName}"; Tasks: desktopicon; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
Name: "{userappdata}\Microsoft\Internet Explorer\Quick Launch\{#MyAppName}"; Filename: "{app}\bin\{#MyAppExeName}"; Tasks: quicklaunchicon; WorkingDir: "{app}\bin"; IconFileName:"{app}\share\frama-c\frama-c.ico"
[Registry]
Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "FRAMAC_SHARE"; ValueData: "{app}\share\frama-c"; Flags: uninsdeletevalue
Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "FRAMAC_LIB"; ValueData: "{app}\lib\frama-c"; Flags: uninsdeletevalue
Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "FRAMAC_PLUGIN"; ValueData: "{app}\lib\frama-c\plugins"; Flags: uninsdeletevalue
Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "OCAMLLIB"; ValueData: "{app}\lib"; Flags: uninsdeletevalue
Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "WHYLIB"; ValueData: "'{app}\lib\why'"; Flags: uninsdeletevalue
Root: HKLM; Subkey: "SYSTEM\CurrentControlSet\Control\Session Manager\Environment"; ValueType: string; ValueName: "ERGOLIB"; ValueData: "{app}\lib\alt-ergo"; Flags: uninsdeletevalue
Frama-C is now installed on your computer.
Note that no C preprocessor is installed by Frama-C itself.
We encourage you to install cygwin from http://cygwin.org and to launch Frama-C tools from a shell which contains "gcc" and the "bin" directory of Frama-C in its path.
/_build
tests/**/result
tests/*/oracle/dune
/aorai_eva_analysis.ml
/Makefile
/*parser*.output
/ptests_local_config.ml
/tests/*/result
/tests/*/result_prove
/top
/Makefile
/tests/*/result
/tests/**/dune
......@@ -5,10 +5,7 @@
dune-project header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
dune header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
configure.ac header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
Makefile header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
Makefile.in header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
*.c header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
*.h header_spec=CEA_LGPL_OR_PROPRIETARY.E_ACSL
......
*~
*.o
*.cm*
*.annot
/*_DEP
/configure
/config.log
/Makefile
/.depend
/config.status
/autom4te.cache
/ptests_local_config.ml
/configure.lineno
/share/*.cm*
/share/*.annot
/share/*_DEP
/share/e-acsl/*.cm*
/share/e-acsl/*.annot
/share/e-acsl/*_DEP
/doc/manuals
/doc/code
/doc/refman/*.out
/doc/refman/*.bbl
/doc/refman/*.blg
......@@ -48,21 +27,6 @@
/doc/userman/*.idx
/doc/userman/*.log
/doc/userman/*.lof
/tests/*/result*/*
.frama-c
META.frama-c-e_acsl
.merlin
.Makefile.plugin.generated
E_ACSL.check_mli_exists
top/
doc/doxygen/doxygen.cfg
doc/doxygen/html
doc/doxygen/warn.log
lib/libeacsl-jemalloc.a
lib/libeacsl-dlmalloc.a
lib/libeacsl-gmp.a
lib/libeacsl-rtl-bittree.a
lib/libeacsl-rtl-segment.a
lib/libeacsl-rtl-bittree-dbg.a
lib/libeacsl-rtl-segment-dbg.a
src/dependencies/dep_eva.ml
/configure
/Makefile
/tests/*/oracle/dune
/tests/*/result
/configure
/Makefile
/tests/*/result
/tests/**/dune
*.cm*
*.o
top/
*.check_mli_exists
.Makefile.plugin.generated
.depend
.merlin
*~
/Makefile
/tests/**/dune
/tests/*/result
/tests/*/result_*
description = "Frama-C Markdown_report plug-in"
version = "@VERSION@"
requires = "frama-c.kernel ppx_deriving ppx_deriving_yojson yojson"
archive(byte) = "top/Markdown_report.cmo"
archive(native) = "top/Markdown_report.cmx"
plugin(native) = "top/Markdown_report.cmxs"
plugin(byte) = "top/Markdown_report.cmo"
package "eva_info" (
requires = "frama-c-markdown_report frama-c-eva"
plugin(native) = "top/eva_info.cmxs"
plugin(byte) = "top/eva_info.cmo"
)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment