[alias] copy of previous git directory

src/plugins/alias/LICENSE.Alias

+
+This file is part of the Frama-C plug-in 'Alias' (alias).
+
+Copyright (C) 2022-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)
+

src/plugins/alias/Makefile

+##########################################################################
+#                                                                        #
+#  This file is part of the Frama-C plug-in 'Alias' (alias).             #
+#                                                                        #
+#  Copyright (C) 2022-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)                       #
+#                                                                        #
+##########################################################################
+
+.PHONY: all build clean
+
+FRAMAC_SHARE:=$(shell frama-c -print-share-path)
+
+sinclude ${FRAMAC_SHARE}/Makefile.common
+
+##########################################################################
+# Build
+
+all:: build frama-c-alias.opam
+
+frama-c-alias.opam: frama-c-alias.opam.template dune-project
+	rm -f $@
+	dune build $@
+
+build::
+	dune build @install
+
+clean:: purge-tests
+	dune clean
+	rm -rf _build .merlin
+
+##########################################################################
+# Tests
+
+include ${FRAMAC_SHARE}/Makefile.testing
+
+##########################################################################
+# Install
+
+include ${FRAMAC_SHARE}/Makefile.installation
+
+##########################################################################
+# Headers
+
+HDRCK_EXTRA:=-headache-config-file ${FRAMAC_SHARE}/headache_config.txt
+include ${FRAMAC_SHARE}/Makefile.headers
+
+SHORT_NAME:=alias
+LONG_NAME:=Alias
+PLUGIN_NAME:=Alias
+FROM_YEAR:=2022
+
+include headers/Makefile.generate-headers
+
+##########################################################################
+# Linting
+
+include ${FRAMAC_SHARE}/Makefile.linting
+
+##########################################################################

src/plugins/alias/README.md

-# Alias - MERCE
+# MERCE
 
 
+GIT project for our collaboration with MERCE
 
-## Getting started
+## Project Members
 
-To make it easy for you to get started with GitLab, here's a list of recommended next steps.
+Julien (Signoles)
+Tristan
+Allan
+Loïc
 
-Already a pro? Just edit this README.md and make it your own. Want to make it easy? [Use the template at the bottom](#editing-this-readme)!
-
-## Add your files
-
-- [ ] [Create](https://docs.gitlab.com/ee/user/project/repository/web_editor.html#create-a-file) or [upload](https://docs.gitlab.com/ee/user/project/repository/web_editor.html#upload-a-file) files
-- [ ] [Add files using the command line](https://docs.gitlab.com/ee/gitlab-basics/add-file.html#add-a-file-using-the-command-line) or push an existing Git repository with the following command:
-
-```
-cd existing_repo
-git remote add origin https://git.frama-c.com/tl228638/alias-merce.git
-git branch -M main
-git push -uf origin main
-```
-
-## Integrate with your tools
-
-- [ ] [Set up project integrations](https://git.frama-c.com/tl228638/alias-merce/-/settings/integrations)
-
-## Collaborate with your team
-
-- [ ] [Invite team members and collaborators](https://docs.gitlab.com/ee/user/project/members/)
-- [ ] [Create a new merge request](https://docs.gitlab.com/ee/user/project/merge_requests/creating_merge_requests.html)
-- [ ] [Automatically close issues from merge requests](https://docs.gitlab.com/ee/user/project/issues/managing_issues.html#closing-issues-automatically)
-- [ ] [Enable merge request approvals](https://docs.gitlab.com/ee/user/project/merge_requests/approvals/)
-- [ ] [Automatically merge when pipeline succeeds](https://docs.gitlab.com/ee/user/project/merge_requests/merge_when_pipeline_succeeds.html)
-
-## Test and Deploy
-
-Use the built-in continuous integration in GitLab.
-
-- [ ] [Get started with GitLab CI/CD](https://docs.gitlab.com/ee/ci/quick_start/index.html)
-- [ ] [Analyze your code for known vulnerabilities with Static Application Security Testing(SAST)](https://docs.gitlab.com/ee/user/application_security/sast/)
-- [ ] [Deploy to Kubernetes, Amazon EC2, or Amazon ECS using Auto Deploy](https://docs.gitlab.com/ee/topics/autodevops/requirements.html)
-- [ ] [Use pull-based deployments for improved Kubernetes management](https://docs.gitlab.com/ee/user/clusters/agent/)
-- [ ] [Set up protected environments](https://docs.gitlab.com/ee/ci/environments/protected_environments.html)
-
-***
-
-# Editing this README
-
-When you're ready to make this README your own, just edit this file and use the handy template below (or feel free to structure it however you want - this is just a starting point!). Thank you to [makeareadme.com](https://www.makeareadme.com/) for this template.
-
-## Suggestions for a good README
-Every project is different, so consider which of these sections apply to yours. The sections used in the template are suggestions for most open source projects. Also keep in mind that while a README can be too long and detailed, too long is better than too short. If you think your README is too long, consider utilizing another form of documentation rather than cutting out information.
-
-## Name
-Choose a self-explaining name for your project.
-
-## Description
-Let people know what your project can do specifically. Provide context and add a link to any reference visitors might be unfamiliar with. A list of Features or a Background subsection can also be added here. If there are alternatives to your project, this is a good place to list differentiating factors.
-
-## Badges
-On some READMEs, you may see small images that convey metadata, such as whether or not all the tests are passing for the project. You can use Shields to add some to your README. Many services also have instructions for adding a badge.
-
-## Visuals
-Depending on what you are making, it can be a good idea to include screenshots or even a video (you'll frequently see GIFs rather than actual videos). Tools like ttygif can help, but check out Asciinema for a more sophisticated method.
-
-## Installation
-Within a particular ecosystem, there may be a common way of installing things, such as using Yarn, NuGet, or Homebrew. However, consider the possibility that whoever is reading your README is a novice and would like more guidance. Listing specific steps helps remove ambiguity and gets people to using your project as quickly as possible. If it only runs in a specific context like a particular programming language version or operating system or has dependencies that have to be installed manually, also add a Requirements subsection.
-
-## Usage
-Use examples liberally, and show the expected output if you can. It's helpful to have inline the smallest example of usage that you can demonstrate, while providing links to more sophisticated examples if they are too long to reasonably include in the README.
-
-## Support
-Tell people where they can go to for help. It can be any combination of an issue tracker, a chat room, an email address, etc.
-
-## Roadmap
-If you have ideas for releases in the future, it is a good idea to list them in the README.
-
-## Contributing
-State if you are open to contributions and what your requirements are for accepting them.
-
-For people who want to make changes to your project, it's helpful to have some documentation on how to get started. Perhaps there is a script that they should run or some environment variables that they need to set. Make these steps explicit. These instructions could also be useful to your future self.
-
-You can also document commands to lint the code or run tests. These steps help to ensure high code quality and reduce the likelihood that the changes inadvertently break something. Having instructions for running tests is especially helpful if it requires external setup, such as starting a Selenium server for testing in a browser.
-
-## Authors and acknowledgment
-Show your appreciation to those who have contributed to the project.
-
-## License
-For open source projects, say how it is licensed.
-
-## Project status
-If you have run out of energy or time for your project, put a note at the top of the README saying that development has slowed down or stopped completely. Someone may choose to fork your project or volunteer to step in as a maintainer or owner, allowing your project to keep going. You can also make an explicit request for maintainers.

src/plugins/alias/abstract_state.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-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)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+
+
+(** Module abstract_state
+
+    implements "points-to" persistent graphs ans Steensgaard's
+   algorithm
+
+    In the graph:
+
+    - Edges are unlabelled.
+
+    - Vertices are labelled by equivalence classes representative
+   (ECR)
+
+    ECR are abstract states for Lval sets (pointers that may be
+   aliased)
+
+
+ *)
+
+module CType : sig
+  (** placeholder for cil types *)
+  type expr (**  expressions *)
+
+  type instr (** instructions *)
+
+  type varinfo (** variable *)
+  
+  type kf (** functions *)  
+end
+
+
+
+module ECR : sig
+  (** module for the equivalence class, cf Steensgaard's paper *)
+  
+
+  (*  following Steensgaard's notations *)
+  type alpha = Tau of tau  | Lambda of lambda
+
+  and tau = Bottom_T | Ref of alpha (* points-to type *)
+
+  and lambda = Bottom_L | Lam of alpha list * alpha list
+
+  
+
+  type t (* type ECR = equivalence class representant *)
+
+
+  (* functions needed for Steensgaard's algorithm *)
+    
+  (*  TODO : do it in a procedural or a functional style ? *)
+    
+  val get_type: t -> tau
+
+  val join : t -> t -> unit (* join of ecr *)
+
+  val cjoin : t -> t -> unit (*  conditional join *)
+
+  val ecr : CType.expr -> t
+
+  val set_type : tau -> tau -> unit
+
+  val unify_T : tau -> tau -> unit
+    
+  val unify_L : lambda -> lambda -> unit
+
+  val pending : tau -> tau list
+  
+  val make_ecr : int -> tau array (* makes an array of [n] Bottom_T *)
+end
+
+
+
+(** module for vertices *)
+module V : sig
+
+  type t   (*  will have a field for ECR.t set *)                                                                 
+  val compare : t -> t -> int                                                
+  val hash : t -> int                                                    
+  val equal : t -> t -> bool                                                                 
+ end
+
+
+(** module for points-to graphs *)
+module G :
+  sig
+    type t
+    (* directed, persistant graph *)
+
+    val add_vertex : t -> V.t -> t
+
+    val add_edge : t -> (V.t * V.t) -> t
+
+    val remove_edge : t -> (V.t * V.t) -> t
+
+    val merge_vertex : t -> V.t -> V.t -> t
+
+    (* todo add more *)
+  end
+
+
+
+(**  interface for module Alias *)
+  
+
+(** type for abstract states aka points-to graphs  *)
+type t = G.t
+
+
+(** type for summary of function, to be determined *)
+type summary 
+
+(** initialisation *)
+  val compute : unit -> unit
+
+(** evaluation of an expression *)
+val eval_expr : t -> CType.expr -> ECR.t
+
+(** abstract semantic of an instruction *)
+val do_instr : t -> CType.instr -> t
+
+(** creation of the summary of a function; first argument is the context of the declaration *)
+val make_summary : t -> CType.kf -> (t * summary)
+
+val fold_stmt : CType.kf -> CType.varinfo -> ECR.t -> 'a -> 'a

src/plugins/alias/dune

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of the Frama-C plug-in 'Alias' (alias).             ;;
+;;                                                                        ;;
+;;  Copyright (C) 2022-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)                       ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+( rule
+  (alias frama-c-configure)
+  (deps (universe))
+  (action ( progn
+            (echo "Alias:" %{lib-available:frama-c-alias.core} "\n")
+            (echo " - Frama-C:" %{lib-available:frama-c.kernel} "\n")
+          )
+  )
+)
+
+( library
+  (optional)
+  (name alias)
+  (public_name frama-c-alias.core)
+  (flags -open Frama_c_kernel :standard)
+  (libraries frama-c.kernel)
+)
+
+( plugin
+  (optional)
+  (name alias) (libraries frama-c-alias.core) (site (frama-c plugins))
+)

src/plugins/alias/dune-project

+(lang dune 3.2)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of the Frama-C plug-in 'Alias' (alias).             ;;
+;;                                                                        ;;
+;;  Copyright (C) 2022-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)                       ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(using dune_site 0.1)
+(generate_opam_files true)
+
+(name frama-c-alias)
+
+(package (name frama-c-alias)
+ (depends
+  ("frama-c" (and (>= 25.0) (< 26.0)))
+ )
+)

src/plugins/alias/headers/Makefile.generate-headers

+##########################################################################
+#                                                                        #
+#  This file is part of the Frama-C plug-in 'Alias' (alias).             #
+#                                                                        #
+#  Copyright (C) 2022-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)                       #
+#                                                                        #
+##########################################################################
+
+YEAR:=$(shell date +%Y)
+
+ifeq (${HEADER_OPEN_SOURCE},yes)
+DEFAULT_HEADER_DIR:=headers/open-source
+else
+DEFAULT_HEADER_DIR:=headers/close-source
+endif
+
+headers/%/LICENSE.${PLUGIN_NAME}: headers/%/LICENSE.template FORCE_LICENSES
+	@sed -e "s/@SHORT_NAME@/${SHORT_NAME}/" \
+			 -e "s/@LONG_NAME@/${LONG_NAME}/" \
+			 -e "s/@FROM_YEAR@/${FROM_YEAR}/" \
+			 -e "s/@YEAR@/${YEAR}/" \
+			 $< > $@
+
+LICENSE.${PLUGIN_NAME}: ${DEFAULT_HEADER_DIR}/LICENSE.${PLUGIN_NAME} FORCE_LICENSES
+	cp $< $@
+
+.PHONY: FORCE_LICENSES
+FORCE_LICENSES:
+
+# Extend headers rule dependencies, make sure to update all license files
+headers: \
+	headers/open-source/LICENSE.${PLUGIN_NAME} \
+	headers/close-source/LICENSE.${PLUGIN_NAME} \
+	LICENSE.${PLUGIN_NAME}

src/plugins/alias/headers/close-source/LICENSE.Alias

+
+This file is part of the Frama-C plug-in 'Alias' (alias).
+
+Copyright (C) 2022-2022
+  CEA (Commissariat à l'énergie atomique et aux énergies
+       alternatives)
+
+All rights reserved.
+Contact CEA LIST for licensing.
+

src/plugins/alias/headers/close-source/LICENSE.template

+
+This file is part of the Frama-C plug-in '@LONG_NAME@' (@SHORT_NAME@).
+
+Copyright (C) @FROM_YEAR@-@YEAR@
+  CEA (Commissariat à l'énergie atomique et aux énergies
+       alternatives)
+
+All rights reserved.
+Contact CEA LIST for licensing.
+

src/plugins/alias/headers/open-source/LICENSE.Alias

+
+This file is part of the Frama-C plug-in 'Alias' (alias).
+
+Copyright (C) 2022-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)
+

src/plugins/alias/headers/open-source/LICENSE.template

+
+This file is part of the Frama-C plug-in '@LONG_NAME@' (@SHORT_NAME@).
+
+Copyright (C) @FROM_YEAR@-@YEAR@
+  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)
+

src/plugins/alias/nix/alias.nix

+{ mk_plugin }:
+
+mk_plugin {
+  plugin-name = "alias" ;
+  plugin-src = fetchGit { shallow=true ; url=./.. ; } ;
+}

src/plugins/alias/nix/ci.sh

+#!/usr/bin/env bash
+
+set -euxo pipefail
+
+DEFAULT=${DEFAULT:-master}
+NIX_TARGET="alias"
+#           <plugin>   /nix       /ci.sh
+PLUGIN_DIR="$(dirname "$(dirname "$(readlink -f "$0")")")"
+
+CURRENT_BRANCH="${CI_MERGE_REQUEST_SOURCE_BRANCH_NAME:-}"
+: "${CURRENT_BRANCH:="${CI_COMMIT_REF_NAME:-}"}"
+: "${CURRENT_BRANCH:="$(git branch --show-current)"}"
+
+# prints
+# - "$CURRENT_BRANCH" if it is a branch name in remote $1,
+# - else "$DEFAULT" if it is set and $DEFAULT is a branch name in remote $1,
+# - else master
+get_matching_branch () {
+  if   git ls-remote --quiet --exit-code "$1" "$CURRENT_BRANCH" >/dev/null 2>/dev/null;
+  then echo "$CURRENT_BRANCH"
+  elif git ls-remote --quiet --exit-code "$1" "$DEFAULT" >/dev/null 2>/dev/null;
+  then echo "$DEFAULT"
+  else echo master
+  fi
+}
+
+TMP_DIR="$(mktemp -d)"
+
+cleanup () {
+  rm -rf $TMP_DIR
+}
+
+trap cleanup EXIT
+
+mkdir -p $TMP_DIR/frama-ci
+frama_ci_repo="$(readlink -f $TMP_DIR/frama-ci)"
+frama_ci_url="git@git.frama-c.com:frama-c/Frama-CI.git"
+frama_ci_branch="$(get_matching_branch "$frama_ci_url")"
+echo "using branch $frama_ci_branch of Frama-CI repo at $frama_ci_repo"
+git clone --depth=1 --branch="$frama_ci_branch" "$frama_ci_url" "$frama_ci_repo"
+
+source $frama_ci_repo/common-plugin-ci.sh

src/plugins/alias/nix/pkgs.nix

+{ frama-c-repo ? builtins.trace "alias: defaulting frama-c-repo to ${toString ../../frama-c}" ../../frama-c }:
+let
+  ocamlOverlay = oself: osuper: {
+    alias = oself.callPackage ./alias.nix {};
+  };
+  overlay = self: super: {
+    ocaml-ng = super.lib.mapAttrs (
+      name: value:
+        if builtins.hasAttr "overrideScope'" value
+        then value.overrideScope' ocamlOverlay
+        else value
+    ) super.ocaml-ng;
+  };
+  pkgs = (import (frama-c-repo + "/nix/pkgs.nix")).appendOverlays [ overlay ];
+in
+pkgs

src/plugins/alias/tests/basic/oracle/test.res.oracle

+[kernel] Parsing test.i (no preprocessing)
+[kernel] Hello world

src/plugins/alias/tests/ptests_config

+DEFAULT_SUITES=basic

src/plugins/alias/tests/test_config

+PLUGIN: alias
+OPT: