Commit c318ad8c authored by Thibault Martin's avatar Thibault Martin
Browse files

Backward compatibility & autoconf

Ensure backwards compatibility with OCaml 4.02.3
Adopt autoconf-based generation for configure/Makefile
parent 41d33741
......@@ -16,3 +16,8 @@
META.frama-c-*
/tests/ptests_config
.merlin
autom4te.cache
config.log
config.status
configure
Makefile
......@@ -2,38 +2,62 @@
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2013-2018 #
# Copyright (C) 2007-2018 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# You may redistribute it and/or modify it under the terms of the GNU #
# 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 3. #
# 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. #
# 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 3 for more #
# details (enclosed in the file LICENSE). #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
FRAMAC_SHARE :=$(shell frama-c.byte -print-path)
FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)
PLUGIN_NAME = LAnnotate
# Do not use ?= to initialize both below variables
# (fixed efficiency issue, see GNU Make manual, Section 8.11)
ifndef FRAMAC_SHARE
FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
endif
ifndef FRAMAC_LIBDIR
FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
endif
PLUGIN_BFLAGS += -warn-error -a
PLUGIN_OFLAGS += -warn-error -a
###################
# Plug-in Setting #
###################
PLUGIN_TESTS_DIRS:= options criteria
PLUGIN_DIR ?=.
PLUGIN_ENABLE:=yes
PLUGIN_NAME:=LAnnotate
PLUGIN_CMO:= options utils ast_const bes simplify annotators wm \
logical partition ldataflow context function statement lloop \
register
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
PLUGIN_TESTS_DIRS:=options criteria
################
# Generic part #
################
PLUGIN_CMO = options utils ast_const bes simplify annotators wm \
logical partition ldataflow context function statement lloop register
include $(FRAMAC_SHARE)/Makefile.dynamic
clean::
$(RM) -rf top
$(RM) -f META.*
$(RM) -f .depend
#####################################
# Regenerating the Makefile on need #
#####################################
ifeq ("$(FRAMAC_INTERNAL)","yes")
CONFIG_STATUS_DIR=$(FRAMAC_SRC)
else
CONFIG_STATUS_DIR=.
endif
$(LAnnotate_DIR)/Makefile: $(LAnnotate_DIR)/Makefile.in \
$(CONFIG_STATUS_DIR)/config.status
cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2018 #
# 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). #
# #
##########################################################################
# Do not use ?= to initialize both below variables
# (fixed efficiency issue, see GNU Make manual, Section 8.11)
ifndef FRAMAC_SHARE
FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
endif
ifndef FRAMAC_LIBDIR
FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
endif
###################
# Plug-in Setting #
###################
PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_LANNOTATE@
PLUGIN_NAME:=LAnnotate
PLUGIN_CMO:= options utils ast_const bes simplify annotators wm \
logical partition ldataflow context function statement lloop \
register
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
PLUGIN_TESTS_DIRS:=options criteria
################
# Generic part #
################
include $(FRAMAC_SHARE)/Makefile.dynamic
#####################################
# Regenerating the Makefile on need #
#####################################
ifeq ("$(FRAMAC_INTERNAL)","yes")
CONFIG_STATUS_DIR=$(FRAMAC_SRC)
else
CONFIG_STATUS_DIR=.
endif
$(LAnnotate_DIR)/Makefile: $(LAnnotate_DIR)/Makefile.in \
$(CONFIG_STATUS_DIR)/config.status
cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
......@@ -11,13 +11,16 @@ LAnnotate is a Frama-C plugin.
Installation
------------
LAnnotate requires Frama-C (Chlorine or latter) to be installed. A patch (Chlorine.patch) is available for LUncov compatibility.
Once Frama-C is installed, compile and install LAnnotate:
LAnnotate requires Frama-C 17 (Chlorine) or later to be installed.
A patch (Chlorine.patch) is available for LUncov compatibility.
Once Frama-C is installed, run autoconf, configure, compile and install
LAnnotate:
autoconf
./configure
make
make install
The second command may need to be run as root (or sudo) depending on your
The last command may need to be run as root (or sudo) depending on your
Frama-C installation.
Usage
......@@ -56,7 +59,7 @@ Authors
- Omar Chebaro
- Mickaël Delahaye
- Michaël Marcozzi
- Thibault Martin
- Thibault Martin
Also many thanks to the rest of LTest's team:
- Nikolai Kosmatov
- Sébastien Bardin
......
......@@ -72,12 +72,10 @@ let annotate_with annotator ?(id=next) ?(collect=nocollect) ast =
let annotate filename names ?(id=next) ?(collect=nocollect) ast =
filen := filename;
let f name =
let ann = Hashtbl.find_opt annotators name in
match ann with
| None ->
Options.warning "unknown annotators `%s`" name
| Some(ann) ->
try
let ann = Hashtbl.find annotators name in
annotate_with ~id ~collect ann ast
with Not_found -> Options.warning "unknown annotators `%s`" name
in
List.iter f names
......
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2018 #
# 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). #
# #
##########################################################################
###########################################
# LAnnotate as a standard Frama-C plug-in #
###########################################
m4_define([plugin_file],Makefile.in)
m4_define([FRAMAC_SHARE_ENV],
[m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
m4_define([FRAMAC_SHARE],
[m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
[m4_esyscmd(frama-c -print-path)])])
m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
check_plugin(lannotate,PLUGIN_RELATIVE_PATH(plugin_file),
[support for lannotate plug-in],yes)
#######################
# Generating Makefile #
#######################
write_plugin_config(Makefile)
......@@ -216,14 +216,15 @@ class computeCombinations = object(self)
let alldefs = List.fold_left (fun acc id -> (id, (Hashtbl.find currentDef id) - 1) :: acc ) [] lvalIds in
(* 3 *)
let nl = List.fold_left (fun acc (vid,nbDef) ->
let normalDefs = List.init nbDef (fun idDef -> (vid,idDef+1)) in
let normalDefs =
Array.to_list (Array.init nbDef (fun idDef -> (vid,idDef+1))) in
let inLoopDefs =
if not (Stack.is_empty inLoopId) && Hashtbl.mem varLoopID (vid,Stack.top inLoopId) then begin
let lid = get_varLoop_id vid (Stack.top inLoopId) in
let currDef = (Hashtbl.find currentDef lid) in
let comingNext = (Hashtbl.find nBVarDefs lid) - currDef + 1 in
let totalDef = Hashtbl.find nBVarDefs vid in
List.init comingNext (fun idDef -> (vid,totalDef+currDef+idDef))
Array.to_list (Array.init comingNext (fun idDef -> (vid,totalDef+currDef+idDef)))
end
else
[]
......
......@@ -317,7 +317,7 @@ let compute_hl () : string =
Hashtbl.add regroup (vid,defId) [ids]
in
List.iter fill !idList;
if String.equal "-" !symb then
if "-" = !symb then
Hashtbl.fold (fun _ seqs str ->
List.fold_left (fun acc s -> "<s" ^ string_of_int s ^"|; ;>,\n" ^ acc ) str seqs
) regroup ""
......
......@@ -26,7 +26,7 @@ let store_label_data out annotations =
let formatter = Format.formatter_of_out_channel out in
Format.fprintf formatter "# id, status, tag, origin_loc, current_loc, emitter, exec_time@.";
let print_one (id, tags, cond, origin_loc) =
let l = String.split_on_char '/' ((fst origin_loc).Lexing.pos_fname) in
let l = Transitioning.String.split_on_char '/' ((fst origin_loc).Lexing.pos_fname) in
let origin_file = List.nth l ((List.length l)-1) in
let origin_line = (fst origin_loc).Lexing.pos_lnum in
(* let us note obviously uncoverable labels as uncoverable
......
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