Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • pub/frama-clang
  • weliveindetail/frama-clang
  • ankit247/frama-clang
  • T-Gruber/frama-clang
4 results
Show changes
Commits on Source (487)
387 additional commits have been omitted to prevent performance issues.
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 3112 additions and 3057 deletions
.gitattributes 0 → 100644
View file @ f720d219
################
# MERGE: union #
################
Changelog merge=union
##################################################
# BINARY/CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
##################################################
*.jpg binary
*.pdf binary
####################################################
# HEADER_SPEC: CEA_LGPL_OR_PROPRIETARY.Frama_Clang #
####################################################
dune-project header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
dune header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
Doxyfile header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
configure.ac header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
*.cpp header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
*.h header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
*.template header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
/share/libc++/* header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
Make* header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
/intermediate_format.ast header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
*.ml header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
*.mli header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
*.sh header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
*.txt header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
/mainpage.dox header_spec=CEA_LGPL_OR_PROPRIETARY.Frama_Clang
########################
# HEADER_SPEC: .ignore #
########################
# Binaries
*.jpg header_spec=.ignore
*.pdf header_spec=.ignore
# CI
/nix/ci.sh header_spec=.ignore
/nix/sources.json header_spec=.ignore
/.gitlab-ci.yml header_spec=.ignore
*.nix header_spec=.ignore
# Doc
/doc/**/* header_spec=.ignore
Changelog header_spec=.ignore
LICENSE header_spec=.ignore
LLVM_REV header_spec=.ignore
README* header_spec=.ignore
VERSION header_spec=.ignore
CHANGELOG.md header_spec=.ignore
DESCRIPTION.md header_spec=.ignore
# Git
.gitattributes header_spec=.ignore
.gitignore header_spec=.ignore
.gitkeep header_spec=.ignore
# Headers
/headers/open-source/* header_spec=.ignore
/headers/closed-source/* header_spec=.ignore
/headers/headache_config.txt header_spec=.ignore
# OCaml
.merlin header_spec=.ignore
*.opam* header_spec=.ignore
# Tests
/tests/**/* header_spec=.ignore
# Misc
/Ast.org header_spec=.ignore
/gdb_commands header_spec=.ignore
/tests_list.txt header_spec=.ignore
/framaCIRGen_src/.clangd header_spec=.ignore
.gitignore
View file @ f720d219
......@@ -34,7 +34,6 @@
/autom4te.cache
/frama_Clang_config.ml
/*.d
/doc
/frama-clang.tar.gz
/tests/*/result/*
/tests/basic/result/*
......@@ -45,7 +44,6 @@
/tests/stl/result/*
/tests/pp/result/*
/tests/ppwp/result/*
/tests/ptests_config
/bin/framaCIRGen
META.frama-c-frama_clang
/Frama_Clang.check_mli_exists
......@@ -56,3 +54,6 @@ META.frama-c-frama_clang
tempirgen
/mine/
/frama-clang-*.tar.gz
_build
/tests/*/oracle/dune
*.idx
.gitlab-ci.yml
View file @ f720d219
################################################################################
### STAGES
stages:
- git-update
- tests
- tests
- distrib
- compatibility
- prepare-release
- release
################################################################################
### DEFAULT JOB PARAMETERS
default:
tags: [nix-v2]
################################################################################
### VARIABLES
variables:
CURRENT: $CI_COMMIT_REF_NAME
DEFAULT: "stable/chromium"
OCAML: "4_08"
FRAMA_CI_OPT: "--override frama-clang:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
#avoid a nix error https://github.com/NixOS/nix/issues/2087
git-update:
stage: git-update
script:
- nix/frama-ci.sh instantiate --eval -A frama-clang.src.outPath
tags:
- nix
DEFAULT: "master"
OCAML: "4.14"
################################################################################
### ONLY/EXCEPT TEMPLATES
.build_template: &manual_template
except:
refs:
- schedules
when: manual
tests-on-llvm-9:
.build_template: &when_schedules
only:
refs:
- schedules
.build_template: &when_release
only:
variables:
- $RELEASE == "yes"
################################################################################
### TESTS
.build_template: &tests_template
stage: tests
script:
- nix/frama-ci.sh build -A frama-clang.tests
tags:
- nix
- ./nix/ci.sh $LLVM_VERSION
tests-on-llvm-10:
stage: tests
tests-auto:
<<: *tests_template
parallel:
matrix:
- LLVM_VERSION: [ "12", "18" ]
tests-manual:
<<: *tests_template
<<: *manual_template
parallel:
matrix:
- LLVM_VERSION: [ "13", "14", "15", "16", "17" ]
################################################################################
### DISTRIB
check-headers:
stage: distrib
variables:
CI_MODE: "check-headers"
script:
- nix/frama-ci.sh build -A frama-clang.on-llvm10.tests
tags:
- nix
when: manual
- ./nix/ci.sh
tests-on-llvm-11:
stage: tests
################################################################################
### CHECK OPAM PACKAGE STATUS
.build_template: &opam_template
tags: [docker]
image: "ocaml/opam:ubuntu-lts-ocaml-$OCAML"
stage: compatibility
variables:
CI_MODE: "check-opam"
EXTRA_PACKAGES: "clang libclang-dev libclang-cpp-dev llvm-dev"
script:
- nix/frama-ci.sh build -A frama-clang.on-llvm11.tests
tags:
- nix
when: manual
- ./nix/ci.sh
tests-on-llvm-13:
stage: tests
check-opam:
<<: *opam_template
<<: *manual_template
check-opam-nightly:
<<: *opam_template
<<: *when_schedules
check-opam-release:
<<: *opam_template
<<: *when_release
################################################################################
### PRE-RELEASE
.build-template: &make_manual
stage: prepare-release
variables:
OUT: "manual"
CI_MODE: "manual"
artifacts:
paths:
- manual/*.pdf
script:
- ./nix/ci.sh
release-manual:
<<: *when_release
<<: *make_manual
force-manual:
<<: *manual_template
<<: *make_manual
check-versions:
<<: *when_release
stage: prepare-release
variables:
CI_MODE: "check-versions"
script:
- ./nix/ci.sh
################################################################################
### RELEASE
release:
<<: *when_release
stage: release
variables:
CI_MODE: "release"
PLUGIN_FULL_NAME: "Frama-Clang"
REPO: "frama-clang"
RELEASE_OPT: "--assume-yes"
MANUAL_DIR: "manual"
script:
- nix/frama-ci.sh build -A frama-clang.on-llvm13.tests
tags:
- nix
- ls -la
- ls manual
- ./nix/ci.sh
CHANGELOG.md 0 → 100644
View file @ f720d219
# Version 0.0.17
- Compatibility with Frama-C 30 Zinc
# Version 0.0.16
- Better handling of ACSL constructions
- Compatibility with Clang 18
- Compatibility with Frama-C 29 Copper
# Version 0.0.15
- Better handling of mixed C/C++ code and `extern "C"` declarations
- Compatibility with Clang 17
- Compatibility with Frama-C 28.x Nickel
# Version <= 0.0.14
- See https://frama-c.com/fc-plugins/frama-clang.html
CMakeLists.txt deleted 100644 → 0
View file @ 67a52f9d
set( LLVM_LINK_COMPONENTS
${LLVM_TARGETS_TO_BUILD}
Option
Support
)
add_clang_executable(framaCIRGen
DescentParse.cpp
ACSLCodeAnnotation.cpp
ACSLComment.cpp
ACSLComponent.cpp
ACSLFunctionContract.cpp
ACSLGlobalAnnotation.cpp
ACSLLexer.cpp
ACSLLogicType.cpp
ACSLLoopAnnotation.cpp
ACSLParser.cpp
ACSLStatementAnnotation.cpp
ACSLTermOrPredicate.cpp
ACSLToken.cpp
Clang_utils.cpp
ClangVisitor.cpp
RTTITable.cpp
VisitTable.cpp
FramaCIRGen.cpp
intermediate_format.c
)
if (CLANG_VERSION VERSION_LESS 6.0.0)
target_link_libraries(framaCIRGen
clangAnalysis
clangAST
clangBasic
clangDriver
clangEdit
clangFrontend
clangLex
clangParse
clangSema
clangSerialization
clangTooling
LLVMBitReader
LLVMMCParser
LLVMOption
)
else()
target_link_libraries(framaCIRGen
PRIVATE
clangAnalysis
clangAST
clangBasic
clangDriver
clangEdit
clangFrontend
clangLex
clangParse
clangSema
clangSerialization
clangTooling
)
endif()
install(TARGETS framaCIRGen
RUNTIME DESTINATION bin)
DESCRIPTION.md 0 → 100644
View file @ f720d219
Frama-Clang is an experimental C++ front-end for Frama-C, based on the clang compiler
Doxyfile
View file @ f720d219
......@@ -2,7 +2,7 @@
/* */
/* This file is part of Frama-Clang */
/* */
/* Copyright (C) 2012-2022 */
/* Copyright (C) 2012-2025 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
......
Frama_Clang.mli → Frama_Clang.ml
View file @ f720d219
......@@ -2,7 +2,7 @@
(* *)
(* This file is part of Frama-Clang *)
(* *)
(* Copyright (C) 2012-2022 *)
(* Copyright (C) 2012-2025 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
LICENSE
View file @ f720d219
Unless otherwise specified, files in this directory are
Copyright (C) 2012-2021
Copyright (C) 2012-2023
CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
......@@ -160,7 +160,7 @@ such a program is covered only if its contents constitute a work based
on the Library (independent of the use of the Library in a tool for
writing it). Whether that is true depends on what the Library does
and what the program that uses the Library does.
1. You may copy and distribute verbatim copies of the Library's
complete source code as you receive it, in any medium, provided that
you conspicuously and appropriately publish on each copy an
......@@ -470,6 +470,3 @@ SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
DAMAGES.
END OF TERMS AND CONDITIONS
LLVM_REV deleted 100644 → 0
View file @ 67a52f9d
# LLVM/Clang revision number against which the plugin has been compiled
179014
Makefile
View file @ f720d219
......@@ -2,7 +2,7 @@
# #
# This file is part of Frama-Clang #
# #
# Copyright (C) 2012-2022 #
# Copyright (C) 2012-2025 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -20,109 +20,48 @@
# #
##########################################################################
### Main Makefile. As Makefiles included from clang and Frama-C are incompatible
### we have two auxiliary Makefiles, one for each side of the front-end.
### We define here general targets that will operate on both sides.
FCLANG_VERSION=0.0.11
PLUGIN_DIR ?= .
include $(PLUGIN_DIR)/Makefile.common
PLUGIN_NAME:=Frama_Clang
PLUGIN_ENABLED:=yes
PLUGIN_CMI:=intermediate_format
PLUGIN_CMO:=intermediate_format_parser frama_Clang_option \
fclang_datatype reorder_defs cxx_utils mangling \
convert_env convert_acsl generate_spec class convert \
convert_link frama_Clang_register
ifneq ("$(MAKECMDGOALS)","uninstall")
PLUGIN_GENERATED:= \
$(addprefix $(PLUGIN_DIR)/, \
intermediate_format_parser.ml \
intermediate_format.mli intermediate_format_parser.mli)
else
PLUGIN_GENERATED:=
endif
PLUGIN_DEPENDENCIES:= wp
ifeq ("$(RUN_TESTS)","yes")
PLUGIN_TESTS_DIRS:=basic stl class val_analysis template specs exn pp ppwp bugs da
else
PLUGIN_NO_TESTS:=yes
.PHONY: all build clean
ifndef FRAMAC_SHARE
FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
endif
PLUGIN_DISTRIBUTED:=no
include $(FRAMAC_SHARE)/Makefile.dynamic
$(Frama_Clang_DIR)/tests/ptests_config: $(Frama_Clang_DIR)/Makefile.config
install::
$(MKDIR) $(FRAMAC_DATADIR)/frama-clang/libc++
$(CP) $(addprefix $(Frama_Clang_DIR)/share/libc++/, \
$(CXX_HEADERS)) \
$(FRAMAC_DATADIR)/frama-clang/libc++
working-tests: $(Frama_Clang_DIR)/ptests_local_config.cmxs
@echo "FRAMAC_SHARE=$(FRAMAC_SHARE)"
LINES=$$(sed -e '/^Tests OK:$$/b out' -e d -e ':out' -e '=' -e 'd' \
$(Frama_Clang_DIR)/tests_list.txt); \
TESTS=$$(tail -n +$$((LINES+1)) \
$(Frama_Clang_DIR)/tests_list.txt | tr '\n' ' '); \
cd $(Frama_Clang_DIR) && $(PTESTS) $(PTESTS_OPTS) $$TESTS
make -C $(Frama_Clang_DIR)
tests:: dontrun
dontrun:
(cd tests; echo `grep -r 'DONTRUN' $(PLUGIN_TESTS_DIRS) | wc -l` test files marked DONTRUN )
$(Frama_Clang_DIR)/gen_ast: $(Frama_Clang_DIR)/gen_ast.ml $(Frama_Clang_DIR)/gen_ast.cmi
$(PRINT_OCAMLC) $@
$(OCAMLC) $(Frama_Clang_BFLAGS) -o $@ -pp $(CAMLP5O) \
zarith.cma dynlink.cma $<
$(Frama_Clang_DIR)/test_ast: \
$(Frama_Clang_DIR)/intermediate_format.cmo \
$(Frama_Clang_DIR)/intermediate_format.o
$(Frama_Clang_DIR)/%_parser.ml $(Frama_Clang_DIR)/%_parser.mli \
$(Frama_Clang_DIR)/%.mli $(Frama_Clang_DIR)/%.c: \
$(Frama_Clang_DIR)/%.ast $(Frama_Clang_DIR)/gen_ast
$(PRINT_MAKING) "intermediate AST"
$(Frama_Clang_DIR)/gen_ast $<
CLANG_MAKE:=$(MAKE) PLUGIN_DIR=$(Frama_Clang_DIR) FRAMAC_SHARE=$(FRAMAC_SHARE) \
-f $(Frama_Clang_DIR)/Makefile.clang
clean::
$(RM) gen_ast
$(CLANG_MAKE) clean
all::
$(CLANG_MAKE) default
install::
@echo "BINDIR is $(BINDIR)"
$(CLANG_MAKE) install
doc::
$(CLANG_MAKE) doc
distrib: clean
$(PRINT_MAKING) $@
$(RM) -r frama-clang
$(MKDIR) frama-clang-$(FCLANG_VERSION)
$(MKDIR) frama-clang-$(FCLANG_VERSION)/bin
$(TAR) cf tmp.tar $(FCLANG_DISTRIBUTED_FILES)
cd frama-clang-$(FCLANG_VERSION) && $(TAR) xf ../tmp.tar
$(TAR) czf frama-clang-$(FCLANG_VERSION).tar.gz frama-clang-$(FCLANG_VERSION)
$(RM) -r frama-clang-$(FCLANG_VERSION)
NOHEADER=$(addprefix $(Frama_Clang_DIR)/, configure README.md)
headers::
$(PRINT_MAKING) $@
headache -c $(Frama_Clang_DIR)/.headache_config.txt \
-h $(Frama_Clang_DIR)/.LICENSE \
$(filter-out $(NOHEADER), $(FCLANG_DISTRIBUTED_FILES))
sinclude ${FRAMAC_SHARE}/Makefile.common
##########################################################################
# Build
all:: build frama-clang.opam
frama-clang.opam: frama-clang.opam.template dune-project
rm -f $@
dune build $@
build::
dune build @install
clean:: purge-tests
dune clean
rm -rf _build .merlin
##########################################################################
# Tests
# PTEST_OPTS has to be defined when Frama-Clang plugin is external
# in order to redefine the macro @FRAMAC_SHARE@ for a FILTER directive
PTEST_OPTS?= -macro-frama-c-share=$(FRAMAC_SHARE)
include ${FRAMAC_SHARE}/Makefile.testing
##########################################################################
# Install
include ${FRAMAC_SHARE}/Makefile.installation
##########################################################################
# Headers
HDRCK_EXTRA:=-headache-config-file ./headers/headache_config.txt
include ${FRAMAC_SHARE}/Makefile.headers
##########################################################################
README.md
View file @ f720d219
......@@ -7,7 +7,7 @@ infrastructure.
The following packages must be present on the system in order to compile
Frama-Clang
- llvm and clang (version >= 6.x, preferably 9 or 10)
- llvm and clang (version >= 11)
- For Ubuntu and Debian, install the following packages:
libclang-<version>-dev clang-<version>
(with their dependencies).
......@@ -16,26 +16,31 @@ Frama-Clang
(packages such as llvm<version>, llvm<version>-devel and ncurses-devel
should be included in their dependencies; otherwise, you might need to
install them as well)
- Frama-C version 21.x Scandium
- OCaml version 4.05 or higher
- Frama-C version 30.x Zinc
- OCaml version 4.14.0 or higher
(i.e. the same version than the one that was used to compile Frama-C).
- The corresponding camlp5 version
- The corresponding `camlp5` version
- `camlp-streams` (available through `opam`, it should normally be installed
together with `camlp5` if needed)
The front-end can then be compiled with the traditional commands
```
./configure
make
make install
```
Depending on the exact configuration of the system,
the last step might require administrator rights. See `./configure --help`
for possible customization of the configuration stage.
Depending on the exact configuration of the system,
the last step might require administrator rights.
`frama-clang` can also be installed directly through `opam`: `opam install frama-clang`. Note
however that you might need to install some of the clang/llvm related packages by hand (see above),
as the `conf-llvm` and `conf-libclang` packages of `opam` do not properly capture all external
dependencies for some distributions.
# Usage
Once installed, Frama-Clang will be automatically called by Frama-C's kernel
whenever a C++ source file is encountered. More precisely, files ending
whenever a C++ source file is encountered. More precisely, files ending
with `.cpp`, `.C`, `.cxx`, `.c++` or `.cc` will be treated as C++ files.
Files ending with `.ii` will be considered as already pre-processed C++ files.
......@@ -55,7 +60,7 @@ Options of the plug-in are the following.
- `-cxx-c++stdlib-path <path>` specifies where to look for
standard C++ library headers (default is the path to Frama-Clang headers,
which are very incomplete)
- `-cxx-nostdinc` do not include in the search paths
- `-cxx-nostdinc` do not include in the search paths
Frama-C's C/C++ standard headers location (i.e. rely on the system's headers)
- `-cxx-clang-command <cmd>` allows changing the name of the
command that launches clang and its plugin that outputs the intermediate AST.
......@@ -74,3 +79,5 @@ fully qualified C++ name (provided it refers to an existing function
in the code under analysis of course). Note however that it is
currently not possible to distinguish between overloaded functions
using this mechanism.
More information is available in the [user manual](https://frama-c.com/download/frama-clang-manual.pdf).
VERSION deleted 100644 → 0
View file @ 67a52f9d
23.0 Vanadium
Makefile.clang → bin/set-version.sh 100644 → 100755
View file @ f720d219
#!/bin/bash
##########################################################################
# #
# This file is part of Frama-Clang #
# #
# Copyright (C) 2012-2022 #
# Copyright (C) 2012-2025 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -20,94 +21,46 @@
# #
##########################################################################
##===- tools/frama-c/Makefile --------------------------*- Makefile -*-===##
#
##===----------------------------------------------------------------------===##
### Clang specific Makefile. Don't call it directly, use the targets from
### main Makefile
### NB: This directory is supposed to be placed in clang/tools, which itself
### should reside in llvm/tools. LLVM Makefile does not seem robust enough to
### support a completely external compilation.
TOOLNAME = framaCIRGen
PLUGIN_DIR ?= .
Frama_Clang_DIR=$(PLUGIN_DIR)
include $(PLUGIN_DIR)/Makefile.common
.PHONY: default clean install doc
OBJS=\
$(addprefix $(PLUGIN_DIR)/, \
Clang_utils.o intermediate_format.o ACSLComment.o ACSLLogicType.o \
ACSLTermOrPredicate.o ACSLLoopAnnotation.o ACSLStatementAnnotation.o\
ACSLGlobalAnnotation.o ACSLCodeAnnotation.o ACSLFunctionContract.o \
ACSLComponent.o ACSLLexer.o ACSLParser.o \
ACSLToken.o DescentParse.o RTTITable.o VisitTable.o \
ClangVisitor.o FramaCIRGen.o)
DEPS=$(OBJS:.o=.d)
CXXFLAGS?=$(CLANG_CXXFLAGS)
CXXFLAGS+=-DCLANG_BIN_DIR=\"$(CLANG_BIN_DIR)\" \
-O1 -Wall -Wno-comment -Wno-enum-compare
CFLAGS?=$(CLANG_CFLAGS)
CFLAGS+=-O1 -Wno-enum-compare
# enabling non-null assertions for AST construction would require
# some refactoring in RTTITable.cpp. Still TODO at this point.
CHECK_AST_CONSTRUCTION?=no
ifeq ("$(CHECK_AST_CONSTRUCTION)","no")
$(Frama_Clang_DIR)/intermediate_format.o: CFLAGS+=-DNDEBUG
endif
ifeq ("$(CLANG_DEBUG)","yes")
CXXFLAGS+=-g
CFLAGS+=-g
CLANG_LINKFLAGS+=-g
endif
LLVM_MAJOR:= $(shell echo $(LLVM_VERSION) | sed -e 's/^\([0-9]*\).*/\1/')
LLVM_MAJOR_10:= \
$(shell if test $(LLVM_MAJOR) -ge 10; then echo "yes"; else echo "no"; fi)
# for use in main Makefile
default: $(PLUGIN_DIR)/bin/$(TOOLNAME)
$(PLUGIN_DIR)/bin/$(TOOLNAME): $(OBJS) $(PLUGIN_DIR)/bin
$(PRINT_LINKING) $@
$(CXX) $(CLANG_LINKFLAGS) -o $@ \
$(OBJS) $(addprefix -l,$(CLANG_LIBS)) $(LLVM_LIBS) $(CLANG_SYSLIBS) $(CLANG_LINKFLAGS)
$(PLUGIN_DIR)/bin:
$(MKDIR) $@
clean:
$(PRINT_RM) 'FramaCIRGen'
rm -f $(PLUGIN_DIR)/bin/$(TOOLNAME) *.o *.d
%.o: %.cpp
$(PRINT) 'Compiling '$<
$(CXX) -c $(CXXFLAGS) -I $(CLANG_INCDIR) -I $(PLUGIN_DIR) \
-MD -MF $(@:.o=.d) -o $@ $<
%.o: %.c
$(PRINT) 'Compiling '$<
$(CC) -c $(CFLAGS) -I $(CLANG_INCDIR) -I $(PLUGIN_DIR) -o $@ $<
install:
$(PRINT_INSTALL) $(TOOLNAME) in $(BINDIR)
$(MKDIR) -p $(BINDIR)
cp $(PLUGIN_DIR)/bin/$(TOOLNAME) $(BINDIR)
doc:
$(PRINT_MAKING) "FramaCIRGen documentation"
cd $(PLUGIN_DIR) && doxygen
cd $(PLUGIN_DIR)/doc/latex && make
-include $(DEPS)
FCLANG_NEXT=$1
FC_NEXT=$2
FC_NEXT_NAME=$3
if ! test -f frama-clang.opam.template; then
echo "This script must be run from Frama-Clang root directory"
exit 2;
fi
if test -z "$FCLANG_NEXT" -o -z "$FC_NEXT" -o -z "$FC_NEXT_NAME"; then
echo "Missing argument. Usage is:"
echo "./bin/set-version.sh fclang-version fc-version fc-version-name"
exit 2;
fi
if command -v gsed &>/dev/null; then
SED=gsed
else
if sed --version 2>/dev/null | grep -q GNU; then
SED=sed
else
echo "GNU sed required"
exit 1
fi
fi
FC_NEXT_ROOT=$($SED -e "s/^\\([0-9]*\.[0-9]*\\).*/\\1/" <<< $FC_NEXT)
FC_NEXT_MAJOR=$($SED -e "s/^\\([0-9]*\\)\..*/\\1/" <<< $FC_NEXT)
if test -z "$FC_NEXT_ROOT" -o -z "FC_NEXT_MAJOR"; then
echo "Unrecognized fc-version number (expecting X.Y)"
exit 2;
fi
FC_NEXT_NEXT_MAJOR=$(($FC_NEXT_MAJOR + 1))
$SED -i -e "s/^ *version: .*/version: \"$FCLANG_NEXT\"/" frama-clang.opam.template
$SED -i -e "s/^ *version: .*/version: \"$FCLANG_NEXT\"/" frama-clang.opam
$SED -i -e "s/(\"frama-c\" .*/(\"frama-c\" (and (>= $FC_NEXT_ROOT~) (< $FC_NEXT_NEXT_MAJOR.0~)))/" dune-project
$SED -i -e "s/- Frama-C version.*/- Frama-C version $FC_NEXT $FC_NEXT_NAME/" README.md
echo $FCLANG_NEXT > doc/userman/FCLANG_VERSION
echo $FC_NEXT > doc/userman/FC_VERSION
echo $FC_NEXT_NAME > doc/userman/FC_VERSION_NAME
class.ml
View file @ f720d219
......@@ -2,7 +2,7 @@
(* *)
(* This file is part of Frama-Clang *)
(* *)
(* Copyright (C) 2012-2022 *)
(* Copyright (C) 2012-2025 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
class.mli
View file @ f720d219
......@@ -2,7 +2,7 @@
(* *)
(* This file is part of Frama-Clang *)
(* *)
(* Copyright (C) 2012-2022 *)
(* Copyright (C) 2012-2025 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
configure.ac deleted 100644 → 0
View file @ 67a52f9d
##########################################################################
# #
# This file is part of Frama-Clang #
# #
# Copyright (C) 2012-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). #
# #
##########################################################################
m4_define([plugin_file],Makefile.config.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([frama_clang],PLUGIN_RELATIVE_PATH(plugin_file),
[C++ front-end for Frama-C],yes)
plugin_require_external(frama_clang,camlp5o)
plugin_use(frama_clang,wp)
# check for system C++ compiler, as we can't rely on clang++ itself because
# of potential incompatibilities with GNU libstdc++ v5.
# See https://llvm.org/bugs/show_bug.cgi?id=23529 for more details
AC_PROG_CXX()
configure_tool([CAMLP5O],[camlp5o],[camlp5o not found.],no)
check_plugin_dependencies()
AC_SUBST(CLANG_CXXFLAGS)
AC_SUBST(CLANG_CFLAGS)
AC_SUBST(CLANG_INCDIR)
AC_SUBST(CLANG_LINKFLAGS)
AC_SUBST(CLANG_SYSLIBS)
AC_SUBST(CLANG_BIN_DIR)
AC_SUBST(LLVM_LIBS)
AC_SUBST(CLANG_LIBS)
AC_SUBST(LLVM_VERSION)
AC_SUBST(DEFAULT_FC_C_HEADERS)
AC_SUBST(DEFAULT_FC_CXX_HEADERS)
AC_SUBST(RUN_TESTS)
DEFAULT_FC_C_HEADERS=$datarootdir/frama-c/libc
DEFAULT_FC_CXX_HEADERS=$datarootdir/libc++
AC_CHECK_PROGS([CLANG],[clang clang-13 clang-12 clang-11 clang-10 clang-9 clang-8 clang-7 clang-6.0],no)
AC_CHECK_PROGS([CLANGXX],[clang++ clang++13 clang++-12 clang++-11 clang++-10 clang++-9 clang++-8 clang++-7 clang++6.0],no)
AC_CHECK_PROGS([LLVM_CONFIG],[llvm-config llvm-config-13 llvm-config-12 llvm-config-11 llvm-config-10 llvm-config-9 llvm-config-8 llvm-config-7 llvm-config-6.0],no)
if test "$LLVM_CONFIG" = "no"; then
plugin_disable(frama_clang,[llvm-config not found]);
fi
if test "$CLANG" = "no"; then
plugin_disable(frama_clang,[clang not found]);
fi
if test "$CLANG++" = "no"; then
plugin_disable(frama_clang,[clang++ not found]);
fi
if test "$ENABLE_FRAMA_CLANG" != "no"; then
LLVM_VERSION=$($LLVM_CONFIG --version)
AC_MSG_CHECKING([LLVM version])
LLVM_SHARED_MODE=$($LLVM_CONFIG --shared-mode)
RUN_TESTS=no
case $LLVM_VERSION in
6.*) AC_MSG_RESULT([$LLVM_VERSION: Good]);;
7.*) AC_MSG_RESULT([$LLVM_VERSION: Good]);;
8.*) AC_MSG_RESULT([$LLVM_VERSION: Good]);;
9.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;;
10.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;;
11.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;;
12.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;;
13.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;;
*) plugin_disable(frama_clang,
[[LLVM Version $LLVM_VERSION is not supported. Please install LLVM 6.x, 7.x, 8.x, 9.x, 10.x, 11.x, 12.x, or 13.x]]);;
esac
LLVM_CONFIG="$LLVM_CONFIG $LLVM_STATIC"
CLANG_CXX_COMMONFLAGS="$($LLVM_CONFIG --cppflags) -fPIC"
CLANG_CFLAGS="$($LLVM_CONFIG --cppflags) -fPIC"
CLANG_INCDIR=$($LLVM_CONFIG --includedir)
CLANG_LINKFLAGS="$($LLVM_CONFIG --ldflags)"
CLANG_CXXFLAGS="$($LLVM_CONFIG --cxxflags) -fPIC -fno-rtti"
CLANG_SYSLIBS="$($LLVM_CONFIG --system-libs)"
CLANG_BIN_DIR="$($LLVM_CONFIG --bindir)"
if test "$LLVM_SHARED_MODE" = "shared"; then
LLVM_LIBS=$($LLVM_CONFIG --libs core);
CLANG_LIBS=clang-cpp
else
LLVM_LIBS=$($LLVM_CONFIG --libs profiledata asmparser mc mcparser support bitreader option);
CLANG_LIBS=clangFrontend clangDriver clangParse clangSema clangAnalysis \
clangEdit clangAST clangLex clangSerialization clangBasic
fi
fi
write_plugin_config(Makefile.config)
convert.ml
View file @ f720d219
This diff is collapsed.
convert.mli
View file @ f720d219
......@@ -2,7 +2,7 @@
(* *)
(* This file is part of Frama-Clang *)
(* *)
(* Copyright (C) 2012-2022 *)
(* Copyright (C) 2012-2025 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
convert_acsl.ml
View file @ f720d219
This diff is collapsed.