Pystan/config/sign_analysis.py

+# pyright: strict
+"""
+implements a sign analysis
+"""
+from enum import Enum, auto
+from dataclasses import dataclass
+from cfg import Cfg
+from iteration import Transfer, fixpoint_iteration
+from syntax import *
+
+class sign(Enum):
+    SNEG = auto()
+    SPOS = auto()
+    Z = auto()
+    NEG = auto()
+    POS = auto()
+    NZ = auto()
+    INT = auto()
+
+class Top:
+    def __str__(self): return "TOP"
+
+@dataclass
+class BTop:
+    """class used for the evaluation of boolean expressions
+
+    BTop(False) indicates that we don't know if the result is True or False, but
+    that the evaluation cannot lead to an error
+    BTop(True) indicates that we neither know the result nor whether an error can occur
+    """
+    has_error: bool
+    def __str__(self):
+        if self.has_error: return "TOP (maybe error)"
+        else: return "TOP (no error)"
+
+type abstract_env = dict[str, sign]
+"""mapping from variables to abstract values.
+
+As with concrete environment, a variable not in the dictionary will
+lead to an error if we try to obtain its value
+"""
+type state = abstract_env | None
+"""abstract state is either an abstract env or bottom
+"""
+
+def sign_leq(v1: sign, v2:sign) -> bool:
+    """order relation on the sign lattice"""
+    if v1 == v2: return True
+    match v1,v2:
+        case _, sign.INT: return True
+        case sign.INT, _: return False
+        case sign.SNEG,(sign.NEG | sign.NZ): return True
+        case sign.SPOS,(sign.POS | sign.NZ): return True
+        case sign.Z,(sign.POS | sign.NEG): return True
+        case sign.NEG,sign.NZ: return True
+        case sign.POS,sign.NZ: return True
+        case _: return False
+
+def sign_join(v1: sign, v2:sign) -> sign:
+    """computes least upper bound"""
+    match v1,v2:
+        case sign.INT, _: return sign.INT
+        case _, sign.INT: return sign.INT
+        case sign.NZ, (sign.NZ | sign.SPOS | sign.SNEG): return sign.NZ
+        case sign.NZ,_: return sign.INT
+        case sign.NEG, (sign.NEG | sign.SNEG | sign.Z): return sign.NEG
+        case sign.NEG, _: return sign.INT
+        case sign.POS, (sign.POS | sign.SPOS | sign.Z): return sign.POS
+        case sign.POS,_: return sign.INT
+        case sign.SNEG, sign.SNEG: return sign.SNEG
+        case sign.SNEG, (sign.Z | sign.NEG): return sign.NEG
+        case sign.SNEG, (sign.SPOS | sign.NZ): return sign.NZ
+        case sign.SNEG, _: return sign.INT
+        case sign.SPOS, sign.SPOS: return sign.SPOS
+        case sign.SPOS, (sign.POS | sign.Z): return sign.POS
+        case sign.SPOS, (sign.SNEG | sign.NZ): return sign.NZ
+        case sign.SPOS, _: return sign.INT
+        case sign.Z, sign.SNEG: return sign.NEG
+        case sign.Z, sign.SPOS: return sign.POS
+        case sign.Z, sign.NZ: return sign.INT
+        case sign.Z, _: return v2
+
+def sign_meet(s1: sign, s2:sign) -> sign | None:
+    """computes greatest lower bound. Can be None (i.e. bottom)"""
+    match s1,s2:
+        case sign.INT, _: return s2
+        case _, sign.INT: return s1
+        case sign.SNEG, (sign.NEG | sign.NZ | sign.SNEG): return s1
+        case (sign.NEG | sign.NZ | sign.SNEG), sign.SNEG: return s2
+        case sign.SNEG, _: return None
+        case _, sign.SNEG: return None
+        case sign.SPOS, (sign.POS | sign.NZ | sign.SPOS): return s1
+        case (sign.POS | sign.NZ | sign.SPOS), sign.SPOS: return s2
+        case sign.SPOS, _: return None
+        case _, sign.SPOS: return None
+        case sign.Z, (sign.NEG | sign.POS): return s1
+        case (sign.NEG | sign.POS), sign.Z: return s2
+        case sign.Z, sign.Z: return s1
+        case sign.Z, _: return None
+        case _, sign.Z: return None
+        case sign.NEG, sign.NEG: return s1
+        case sign.POS, sign.POS: return s1
+        case sign.NEG, sign.POS: return sign.Z
+        case sign.POS, sign.NEG: return sign.Z
+        case sign.NZ, sign.NEG: return sign.SNEG
+        case sign.NEG, sign.NZ: return sign.SNEG
+        case sign.NZ, sign.POS: return sign.SPOS
+        case sign.POS, sign.NZ: return sign.SPOS
+        case sign.NZ, sign.NZ: return sign.NZ
+
+def sign_opp(s:sign) -> sign:
+    """unary minus"""
+    match s:
+        case sign.SNEG: return sign.SPOS
+        case sign.SPOS: return sign.SNEG
+        case sign.POS: return sign.NEG
+        case sign.NEG: return sign.POS
+        case _: return s
+
+def sign_add(s1:sign,s2:sign) -> sign:
+    """addition"""
+    match (s1,s2):
+        case sign.INT,_: return sign.INT
+        case _,sign.INT: return sign.INT
+        case sign.Z,_: return s2
+        case _,sign.Z: return s1
+        case sign.SNEG, (sign.SNEG | sign.NEG): return sign.SNEG
+        case (sign.SNEG | sign.NEG), sign.SNEG: return sign.SNEG
+        case sign.NEG, sign.NEG: return sign.NEG
+        case sign.SPOS, (sign.SPOS | sign.POS): return sign.SPOS
+        case (sign.SPOS | sign.POS), sign.SPOS: return sign.SPOS
+        case sign.POS, sign.POS: return sign.POS
+        case _: return sign.INT
+
+def sign_mul(s1: sign, s2: sign) -> sign:
+    """multiplication"""
+    match s1,s2:
+        case sign.INT,_: return sign.INT
+        case _,sign.INT: return sign.INT
+        case sign.Z,_: return sign.Z
+        case _,sign.Z: return sign.Z
+        case sign.SPOS, _: return s2
+        case _, sign.SPOS: return s1
+        case sign.SNEG, _: return sign_opp(s2)
+        case _,sign.SNEG: return sign_opp(s1)
+        case sign.NZ, _: return sign.INT
+        case _, sign.NZ: return sign.INT
+        case sign.NEG, sign.NEG: return sign.POS
+        case sign.NEG, sign.POS: return sign.NEG
+        case sign.POS, sign.NEG: return sign.NEG
+        case sign.POS, sign.POS: return sign.POS
+
+def sign_div(s1: sign, s2: sign) -> sign | Top | None:
+    """division: can lead to errors even if operands are plain sign"""
+    match s1, s2:
+        case _,sign.Z: return None
+        case _,sign.INT: return Top()
+        case _,sign.POS: return Top()
+        case _,sign.NEG: return Top()
+        case sign.Z,_: return sign.Z
+        case sign.INT,_: return sign.INT
+        case sign.NZ,_: return sign.INT
+        case _,sign.NZ: return sign.INT
+        case (sign.POS | sign.SPOS), sign.SPOS: return sign.POS
+        case (sign.NEG | sign.SNEG), sign.SPOS: return sign.NEG
+        case (sign.POS | sign.SPOS), sign.SNEG: return sign.NEG
+        case (sign.NEG | sign.SNEG), sign.SNEG: return sign.POS
+
+def eval_aexp(env: abstract_env, e: ArithExpr) -> sign | Top | None:
+    """evaluate an arithmetic expression in an abstract environment
+    returns None in case of error
+    """
+    match e:
+        case AECst(value):
+            raise NotImplementedError
+        case AEVar(var):
+            raise NotImplementedError
+        case AEUop(uop,expr):
+            raise NotImplementedError
+        case AEBop(bop,left_expr,right_expr):
+            raise NotImplementedError
+        case _: pass
+
+def eval_bexp(env: abstract_env, e: BoolExpr) -> bool | BTop | None:
+    """abstract evaluation of a boolean expression"""
+    match e:
+        case BEPlain(aexpr):
+            raise NotImplementedError
+        case BEEq(left_expr,right_expr):
+            raise NotImplementedError
+        case BELeq(left_expr,right_expr):
+            raise NotImplementedError
+        case BENeg(expr):
+            raise NotImplementedError
+        case _: pass
+
+def reduce_eq_sign(s: state, x: str, expr: ArithExpr) -> state:
+    """reduce the value associated to x in s under the hypothesis that x == expr"""
+    if s is None: return None
+    v = eval_aexp(s,expr)
+    if v is None: return None
+    if isinstance(v,Top): return s
+    res = sign_meet(s[x],v)
+    if res is None: return None
+    return s | { x: res }
+
+def reduce_neq_sign(s: state, x: str, expr: ArithExpr) -> state:
+    """reduce the value associated to x in s under the hypothesis that x != expr"""
+    if s is None: return None
+    v = eval_aexp(s,expr)
+    if v is None: return None
+    if isinstance(v,Top): return s
+    match s[x],v:
+        case sign.POS, sign.Z: return s | { x: sign.SPOS }
+        case sign.NEG, sign.Z: return s | { x: sign.SNEG }
+        case sign.INT, sign.Z: return s | { x: sign.NZ }
+        case _: return s
+
+def reduce_upper_bound(s: state, x: str, expr: ArithExpr) -> state:
+    """reduce the value associated to x in s under the hypothesis that x <= expr"""
+    if s is None: return None
+    v = eval_aexp(s,expr)
+    if v is None: return None
+    if isinstance(v,Top): return s
+    upper = sign.INT
+    match v:
+        case sign.NEG | sign.SNEG:
+            upper = v
+        case sign.Z:
+            upper = sign.NEG
+        case _: pass
+    res = sign_meet(s[x],upper)
+    if res is None: return None
+    return s | { x: res }
+
+def reduce_strict_upper_bound(s: state, x: str, expr: ArithExpr) -> state:
+    """reduce the value associated to x in s under the hypothesis that x < expr"""
+    if s is None: return None
+    v = eval_aexp(s,expr)
+    if v is None: return None
+    if isinstance(v,Top): return s
+    match v:
+        case sign.NEG | sign.SNEG | sign.Z:
+            upper = sign.SNEG
+        case _:
+            upper = sign.INT
+    res = sign_meet(s[x],upper)
+    if res is None: return None
+    return s | { x: res }
+
+def reduce_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
+    """reduce the value associated to x in s under the hypothesis that x >= expr"""
+    if s is None: return None
+    v = eval_aexp(s,expr)
+    if v is None: return None
+    if isinstance(v,Top): return s
+    lower = sign.INT
+    match v:
+        case sign.POS | sign.SPOS:
+            lower = v
+        case sign.Z:
+            lower = sign.POS
+        case _: pass
+    res = sign_meet(s[x],lower)
+    if res is None: return None
+    return s | { x: res }
+
+def reduce_strict_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
+    """reduce the value associated to x in s under the hypothesis that x > expr"""
+    if s is None: return s
+    v = eval_aexp(s,expr)
+    if v is None: return None
+    if isinstance(v,Top): return s
+    match v:
+        case sign.POS | sign.SPOS | sign.Z:
+            lower = sign.SPOS
+        case _:
+            lower = sign.INT
+    res = sign_meet(s[x],lower)
+    if res is None: return None
+    return s | { x: res }
+
+def reduce_state(s: state,c: BoolExpr) -> state:
+    if s is None: return s
+    match c:
+        # To be completed (see course's slides)
+        case _: return s
+
+class Sign_interp(Transfer[state]):
+    variables: frozenset[str]
+    def __init__(self,instr: Instr):
+        self.variables = variables_of_instr(instr)
+    def bottom(self) -> state:
+        return None
+    def init_state(self) -> state:
+        return dict.fromkeys(self.variables, sign.INT)
+    def join(self,s1:state,s2:state) -> state:
+        if s1 is None: return s2
+        if s2 is None: return s1
+        res: abstract_env = {}
+        for var in self.variables:
+            v1 = s1[var]
+            v2 = s2[var]
+            res[var] = sign_join(v1,v2)
+        return res
+
+    def included(self,s1: state,s2: state) -> bool:
+        if s1 is None: return True
+        if s2 is None: return False
+        for var in self.variables:
+            if not sign_leq(s1[var], s2[var]): return False
+        return True
+
+    def tr_skip(self,s: state) -> state:
+        return s
+
+    def tr_set(self,s: state,v: str,e: ArithExpr) -> state:
+        raise NotImplementedError
+
+    def tr_test(self,s: state,c: BoolExpr) -> state:
+        raise NotImplementedError
+
+    def tr_err(self,s: state,e: Expr) -> state:
+        if s is None: return s
+        if isinstance(e,ArithExpr):
+            raise NotImplementedError
+        if isinstance(e,BoolExpr):
+            raise NotImplementedError
+
+def analyze(i: Instr) -> None:
+    cfg = Cfg(i)
+    res = fixpoint_iteration(Sign_interp(i), cfg)
+    for node in cfg.g.nodes:
+        print(f"State at {node}:")
+        s = res[node]
+        if s is not None:
+            for (v, s) in s.items():
+                print(f"  {v}: {s}")

Pystan/config/syntax.py

+"""Nodes of the abstract syntax tree of the program:
+
+- Uop/Bop represent unary/binary arithmetic operator
+- ArithExpr and its children describe arithmetic expressions
+- BoolExpr and its children describe boolean expressions
+- Instr and its children describe instruction
+
+"""
+from enum import Enum
+from dataclasses import dataclass
+
+class Uop(Enum):
+    """unary operators. Currently only unary minus"""
+    OPP = 1
+    def __str__(self):
+        if self is Uop.OPP:
+            return "-"
+        return ""
+
+class Bop(Enum):
+    """binary operators: addition, multiplication, and division"""
+    ADD = 1
+    MUL = 2
+    DIV = 3
+    def __str__(self):
+        match self:
+            case Bop.ADD: return "+"
+            case Bop.MUL: return "*"
+            case Bop.DIV: return "/"
+
+class Expr:
+    """generic class for expressions, either arithmetic or boolean"""
+    pass
+
+@dataclass
+class ArithExpr(Expr):
+    """generic class for arithmetic expressions"""
+    pass
+
+@dataclass
+class AECst(ArithExpr):
+    """integer constants"""
+    value: int
+    def __str__(self):
+        return f"{self.value}"
+
+@dataclass
+class AEVar(ArithExpr):
+    """variables"""
+    var: str
+    def __str__(self):
+        return self.var
+
+@dataclass
+class AEUop(ArithExpr):
+    """unary operation"""
+    uop: Uop
+    expr: ArithExpr
+    def __str__(self):
+        return f"{self.uop}{self.expr}"
+
+@dataclass
+class AEBop(ArithExpr):
+    """binary operation"""
+    bop: Bop
+    left_expr: ArithExpr
+    right_expr: ArithExpr
+    def __str__(self):
+        #TODO: only put parentheses if necessary
+        return f"({self.left_expr}) {self.bop} ({self.right_expr})"
+
+@dataclass
+class BoolExpr(Expr):
+    """generic class for boolean expressions"""
+    pass
+
+@dataclass
+class BEPlain(BoolExpr):
+    """arithmetic expression (true if not 0)"""
+    aexpr: ArithExpr
+    def __str__(self):
+        return f"{self.aexpr}"
+
+@dataclass
+class BEEq(BoolExpr):
+    """equality between two arithmetic expression"""
+    left_expr: ArithExpr
+    right_expr:ArithExpr
+    def __str__(self):
+        return f"{self.left_expr} = {self.right_expr}"
+
+@dataclass
+class BELeq(BoolExpr):
+    """less or equal"""
+    left_expr: ArithExpr
+    right_expr: ArithExpr
+    def __str__(self):
+        return f"{self.left_expr} <= {self.right_expr}"
+
+@dataclass
+class BENeg(BoolExpr):
+    """Negation"""
+    expr: BoolExpr
+    def __str__(self):
+        return f"!{self.expr}"
+
+class Instr:
+    """generic class for instruction"""
+    pass
+
+@dataclass
+class ISkip(Instr):
+    """Skip (do nothing)"""
+    def __str__(self):
+        return "skip"
+
+@dataclass
+class ISet(Instr):
+    """assignment to a variable"""
+    var: str
+    expr: ArithExpr
+    def __str__(self):
+        return f"{self.var} := {self.expr}"
+
+@dataclass
+class ISeq(Instr):
+    """sequence of two instructions"""
+    first: Instr
+    second: Instr
+    def __str__(self):
+        return f"{self.first};\n{self.second}"
+
+@dataclass
+class ICond(Instr):
+    """if then else"""
+    cond: BoolExpr
+    true_branch: Instr
+    false_branch: Instr
+    def __str__(self):
+        return f"if {self.cond} then\n{self.true_branch}\nelse\n{self.false_branch}\nfi"
+
+@dataclass
+class ILoop(Instr):
+    """while loop"""
+    cond: BoolExpr
+    body: Instr
+    def __str__(self):
+        return f"while {self.cond} do\n{self.body}\ndone"
+
+def variables_of_aexpr(e: ArithExpr) -> frozenset[str]:
+    """return the set of variables appearing in the expression"""
+    match e:
+        case AECst(_): return frozenset()
+        case AEVar(var): return frozenset(var)
+        case AEUop(expr=e): return variables_of_aexpr(e)
+        case AEBop(left_expr=le,right_expr=re):
+            return variables_of_aexpr(le) | variables_of_aexpr(re)
+        case _: assert False
+
+def variables_of_bexpr(e: BoolExpr) -> frozenset[str]:
+    """return the set of variable appearing in the expression"""
+    match e:
+        case BEPlain(expr): return variables_of_aexpr(expr)
+        case BEEq(left_expr=le,right_expr=re):
+            return variables_of_aexpr(le) | variables_of_aexpr(re)
+        case BELeq(left_expr=le,right_expr=re):
+            return variables_of_aexpr(le) | variables_of_aexpr(re)
+        case BENeg(expr):
+            return variables_of_bexpr(expr)
+        case _: assert False
+
+def variables_of_instr(instr: Instr) -> frozenset[str]:
+    """return the set of variables appearing in a program"""
+    match instr:
+        case ISkip(): return frozenset()
+        case ISet(var=v,expr=e):
+            return frozenset([v]) | variables_of_aexpr(e)
+        case ISeq(first=i1,second=i2):
+            return variables_of_instr(i1) | variables_of_instr(i2)
+        case ICond(cond=c,true_branch=tb,false_branch=fb):
+            vbranches = variables_of_instr(tb) | variables_of_instr(fb)
+            return variables_of_bexpr(c) | vbranches
+        case ILoop(cond=c,body=b):
+            return variables_of_bexpr(c) | variables_of_instr(b)
+        case _ : assert False

Pystan/flake.lock

+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1739736696,
+        "narHash": "sha256-zON2GNBkzsIyALlOCFiEBcIjI4w38GYOb+P+R4S8Jsw=",
+        "rev": "d74a2335ac9c133d6bbec9fc98d91a77f1604c1f",
+        "revCount": 754461,
+        "type": "tarball",
+        "url": "https://api.flakehub.com/f/pinned/NixOS/nixpkgs/0.1.754461%2Brev-d74a2335ac9c133d6bbec9fc98d91a77f1604c1f/01951426-5a87-7b75-8413-1a0d9ec5ff04/source.tar.gz"
+      },
+      "original": {
+        "type": "tarball",
+        "url": "https://flakehub.com/f/NixOS/nixpkgs/0.1.%2A.tar.gz"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

Pystan/flake.nix

+{
+  description = "A Nix-flake-based Python development environment";
+
+  inputs.nixpkgs.url = "https://flakehub.com/f/NixOS/nixpkgs/0.1.*.tar.gz";
+
+  outputs = { self, nixpkgs }:
+    let
+      supportedSystems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ];
+      forEachSupportedSystem = f: nixpkgs.lib.genAttrs supportedSystems (system: f {
+        pkgs = import nixpkgs { inherit system; };
+      });
+    in
+    {
+      devShells = forEachSupportedSystem ({ pkgs }: {
+        default = pkgs.mkShell {
+          venvDir = ".venv";
+          packages = with pkgs; [ python312 ] ++
+            (with pkgs.python312Packages; [
+              pip
+              venvShellHook
+	      basedpyright
+            ]);
+        };
+      });
+    };
+}

Pystan/tp.md

+# Analyse Statique de Programmes -- TP Analyse Statique
+
+CentraleSupélec
+
+Enseignant: Virgile Prevosto
+
+## Préliminaires
+
+Ce TP utilise exclusivement Python. On pourra utiliser l'image Docker, comme
+au TP précédent, ou directement sa machine si Python y est installé.
+
+### Rappel Docker
+L'image est ici: https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl et peut être utilisée soit localement, soit depuis `MyDocker`. De plus le répertoire  `config` est monté automatiquement dans le container docker si vous utilisez les scripts associé ([PowerShell](https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl/blob/main/start-3asl.ps1) pour Windows ou [sh](https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl/blob/main/start-3asl.sh) pour Linux/macOS/BSD). Ces scripts devraient automatiquement ouvrir un onglet de votre navigateur web avec une session IceWM. Si ce n'est pas le cas, vous pouvez le faire manuellement: http://localhost:3000
+
+NB: l'interpréteur Python est `python3` et non `python`.
+
+### Typage statique
+Les fichiers proposés ont des annotations de types permettant de vérifier que
+les programmes sont bien typés avant de les exécuter. On pourra utiliser
+l'outil [`pyright`](https://microsoft.github.io/pyright/#/) pour la vérification. Il n'est pas présent sur l'image
+Docker, mais peut s'installer via les commandes suivantes:
+```sh
+sudo apt update
+sudo apt install pipx
+sudo apt install pyright
+```
+
+Il dispose également d'un plugin vscode.
+
+## Introduction
+
+Le fichier [syntax.py](config/syntax.py) définit les différentes classes
+syntaxique du langage While vu en cours, soit les expressions arithmétiques,
+les expressions booléennes et les instructions.
+
+## Sémantique opérationnelle
+Le fichier [opsem.py](config/opsem.py) donne un squelette des fonctions à
+écrire pour définir un interpréteur concret du langage While. Les fonctions
+`eval_aexpr`, et `eval_bexpr` permettent d'évaluer respectivement une
+expression arithmétique et une expression booléenne dans un environnement
+qui associe à des noms de variable une valeur entière. En cas d'erreur
+dans l'évaluation d'une (sous-)expression, on renverra None. La fonction `eval_instr`, renvoie l'environnement final obtenu en évaluant dans un environnement initial une instruction donnée. Là encore, en cas d'erreur au cours de l'évaluation, on renvoie `None`.
+
+Compléter ces définitions, et tester le résultat à l'aide du fichier
+[example_opsem.py](config/example_opsem.py), qui définit le programme de calcul de la factorielle,
+et l'évalue pour `x = 4`.
+
+## Calcul de point fixe
+
+Le fichier [cfg.py](config/cfg.py) est donné. Il contient la définition des
+différents labels des arêtes du graphe de flot de contrôle (skip, affectation,
+test, et erreur). On a aussi une classe pour les nœuds, pour un graphe, et pour
+un CFG proprement dit, qui ajoute au graphe les informations sur le nœud
+initial, le nœud final, et le nœud d'erreur. Un CFG est construit à partir d'un
+programme, et cette construction est donnée également.
+
+Le fichier [iteration.py](config/iteration.py) contient une classe abstraite
+`Transfer` qui permet d'implémenter des analyses statiques en donnant l'élément
+`bottom` du treillis, l'état initial, le `join` de deux états, le test
+d'inclusion, et les fonctions de transfert pour chaque étiquette.
+
+Compléter la fonction `fixpoint_iteration` de ce fichier, qui prend en argument
+une instance de `Transfer` et un CFG, et calcule le point fixe associant à
+chaque nœud du CFG l'état correspondant. L'algorithme est le suivant (on ne se
+préoccupe pas de terminaison):
+
+1. le mapping initial associe l'état initial au nœud initial, et `bottom` à tous
+   les autres. On met toutes les arêtes qui partent du nœud initial dans la
+   worklist.
+2. tant que la worklist n'est pas vide, on prend son premier élément, une arête
+qui va du nœud `src` au nœud `dst` avec le label `l`.
+3. on associe au nœud `dst` le `join` de son état actuel avec le résultat
+de la fonction de transfert pour `l` appliqué à l'état associé à `src`
+4. si le nouvel état est inclus dans l'état associé précédemment à `dst`, on
+ne fait rien. Sinon, on ajoute les arêtes qui sortent de `dst` à la worklist
+5. on revient en 2
+
+NB: en pratique, une itération efficace sélectionne l'arête d'intérêt de manière
+beaucoup plus précise, mais cela sort du cadre de ce TP.
+
+Tester le résultat avec le fichier
+[example_iteration.py](config/example_iteration.py), qui définit une analyse
+statique minimaliste, qui propage un état non vide dans tous les nœuds sauf ceux
+qui sont gardés par une condition qui s'évalue à `False` dans un environnement
+vide. Le programme exemple a un CFG qui contient de telles arêtes. À quoi
+correspondent les nœuds indiqués comme inatteignables par l'analyse?
+
+## Propagation de constantes
+
+Le fichier [constant_propagation.py](config/constant_propagation.py) vise à
+implémenter la propagation de constantes dans le cadre défini précédemment.
+Pour cela, on donne un type de valeurs abstraites qui sont soit un entier (quand
+on est sûr qu'une variable est associé à cet entier), soit `None`, pour indiquer
+que plusieurs valeurs sont possibles. Un environnement abstrait associe à des
+variables des valeurs abstraites, et notre état sera un environnement abstrait
+ou `None` pour indiquer que le nœud associé n'est jamais atteint. On donne
+également les fonctions d'évaluation abstraite des expressions, dans un
+environnement abstrait et qui renvoient une valeur abstraite ou `None` si une
+erreur se produit.
+
+Implémenter les différentes méthodes de la classe `Constant_propagation`. On
+définira un état initial où toutes les variables utilisées dans le programme
+sont associées à la valeur `abstract_value(None)`, indiquant qu'elles sont
+présentes dans l'environnement mais peuvent avoir n'importe quelle valeur.
+
+On testera le résultat à l'aide du fichier
+[example_constant_propagation.py](config/example_constant_propagation.py), qui
+définit un programme dont les variables reçoivent des valeurs constantes.  NB:
+pour que l'analyseur arrive à montrer que `c` est constante en fin de programme,
+il faut raffiner la fonction de transfert du `test`, en réduisant l'état propagé
+quand le test est une égalité entre une variable et une expression qui s'évalue
+à une constante, pour tenir compte du fait que dans la branche correspondante,
+la variable est associée à une constante. Ce raffinement est facultatif.

config/cert_exp_33.c

+#include <stddef.h>
+
 void set_flag(int number, int *sign_flag) {
   if (NULL == sign_flag) {
     return;
   }
 
-  if (number > 0) {
+  // if (number > 0) {
+  // Correcte code
+  if (number >= 0) {
     *sign_flag = 1;
   } else if (number < 0) {
     *sign_flag = -1;
   }
+  Frama_C_show_each_set_flag(number, *sign_flag);
 }
 
 int is_negative(int number) {
   int sign;
   set_flag(number, &sign);
+  Frama_C_show_each_is_negative(number, sign);
   return sign < 0;
 }

config/cert_exp_33_realloc.c

-#include <stdlib.h>
 #include <stdio.h>
+#include <stdlib.h>
 enum { OLD_SIZE = 10, NEW_SIZE = 20 };
 
 int *resize_array(int *array, size_t count) {
@@ -8,6 +8,7 @@ int *resize_array(int *array, size_t count) {
   }
 
   int *ret = (int *)realloc(array, count * sizeof(int));
+  //@ split ret==0;
   if (!ret) {
     free(array);
     return 0;

config/cert_exp_33_realloc_compliant.c

+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+enum { OLD_SIZE = 10, NEW_SIZE = 20 };
+
+int *resize_array(int *array, size_t old_count, size_t new_count) {
+  if (0 == new_count) {
+    return 0;
+  }
+
+  int *ret = (int *)realloc(array, new_count * sizeof(int));
+  //@ split ret==0;
+  if (!ret) {
+    free(array);
+    return 0;
+  }
+
+  if (new_count > old_count) {
+    memset(ret + old_count, 0, (new_count - old_count) * sizeof(int));
+  }
+
+  return ret;
+}
+
+void func(void) {
+
+  int *array = (int *)malloc(OLD_SIZE * sizeof(int));
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < OLD_SIZE; ++i) {
+    array[i] = i;
+  }
+
+  array = resize_array(array, OLD_SIZE, NEW_SIZE);
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < NEW_SIZE; ++i) {
+    printf("%d ", array[i]);
+  }
+}

config/cwe20.c

 #include <stdio.h>
 #include <stdlib.h>
-void die(const char* s) {
-    printf("%s",s);
-    exit(2);
+void die(const char *s) {
+  printf("%s", s);
+  exit(2);
 }
 
 #define MAX_DIM 15
@@ -11,27 +11,30 @@ typedef int board_square_t;
 
 /* board dimensions */
 
-int main () {
-    int m,n, error;
-    board_square_t *board;
-    printf("Please specify the board height: \n");
-    error = scanf("%d", &m);
-    if ( EOF == error ){
+int main() {
+  int m, n, error;
+  board_square_t *board;
+  printf("Please specify the board height: \n");
+  error = scanf("%d", &m);
+  if (EOF == error) {
     die("No integer passed: Die evil hacker!\n");
-    }
-    printf("Please specify the board width: \n");
-    error = scanf("%d", &n);
-    if ( EOF == error ){
+  }
+  printf("Please specify the board width: \n");
+  error = scanf("%d", &n);
+  if (EOF == error) {
     die("No integer passed: Die evil hacker!\n");
-    }
-    if ( m > MAX_DIM || n > MAX_DIM ) {
+  }
+  if (m > MAX_DIM || n > MAX_DIM) {
     die("Value too large: Die evil hacker!\n");
+  }
+  board = (board_square_t *)malloc(m * n * sizeof(board_square_t));
+  for (int i = 0; i < m; i++) {
+    for (int j = 0; j < n; j++) {
+      board[n * i + j] = 0;
     }
-    board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
-    for (int i = 0; i < m; i++) {
-        for (int j = 0; j < n; j++) {
-            board[n*i+j] = 0;
-        }
-    }
-    if (board[(m-1)*n] == 0) return 0; else return 1;
+  }
+  if (board[(m - 1) * n] == 0)
+    return 0;
+  else
+    return 1;
 }

config/cwe20_compliant.c

+#include <stdio.h>
+#include <stdlib.h>
+void die(const char *s) {
+  printf("%s", s);
+  exit(2);
+}
+
+#define MAX_DIM 15
+
+typedef int board_square_t;
+
+/* board dimensions */
+
+int main(void) {
+  unsigned int m, n, error;
+  board_square_t *board;
+  printf("Please specify the board height: \n");
+  error = scanf("%d", &m);
+  if (EOF == error) {
+    die("No integer passed: Die evil hacker!\n");
+  }
+  printf("Please specify the board width: \n");
+  error = scanf("%d", &n);
+  if (EOF == error) {
+    die("No integer passed: Die evil hacker!\n");
+  }
+  if (m > MAX_DIM || m <= 0 || n > MAX_DIM) {
+    die("Value too large: Die evil hacker!\n");
+  }
+
+  board = (board_square_t *)malloc(m * n * sizeof(board_square_t));
+
+  // Check that is memory is properly allocated
+  if (!board) {
+    return 2;
+  }
+
+  for (unsigned int i = 0; i < m; i++) {
+    for (unsigned int j = 0; j < n; j++) {
+      board[n * i + j] = 0;
+    }
+  }
+
+  //@ split m == 0;
+  if (board[(m - 1) * n] == 0)
+    return 0;
+  else
+    return 1;
+}

config/libstring.c

-#include <string.h>
-#include <stdlib.h>
-#include <ctype.h>
+#include <__fc_builtin.h>
 #include <assert.h>
-#include <unistd.h>
+#include <ctype.h>
 #include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
 
-
-#define unlikely(x)    __builtin_expect(!!(x), 0)
+#define unlikely(x) __builtin_expect(!!(x), 0)
 
 #include "libstring.h"
 
 #define BUF_LEN 65536
 #define CAP_DEFAULT 10
 
+int main(void) {
+  char char_string1[255];
+  char char_string2[255];
+  for (int i = 0; i < 254; i++) {
+    char_string1[i] = Frama_C_interval(1, 127);
+    char_string2[i] = Frama_C_interval(1, 127);
+  }
+  char_string1[254] = '\0';
+  char_string2[254] = '\0';
+  string_t *string1 = string_new(char_string1);
+  string_t *string2 = string_new(char_string2);
+  if (!string1 || !string2) {
+    printf("Invalid strings before concatenation !");
+    return -2;
+  }
+  string_t *string_final = string_concat(string1, string2);
+  free(string1);
+  free(string2);
+  if (!string_final) {
+    printf("Invalid string after concatenation !");
+    return -1;
+  }
+  string_print(string_final);
+  free(string_final);
+
+  /**********************************************************************/
+
+  string_t *original = string_new("Hello world");
+  string_t *substring_old = string_new("world");
+  string_t *substring_new = string_new("Paris");
+
+  if (!original || !substring_old || !substring_new) {
+    printf("Invalid strings before substitution !");
+    return -2;
+  }
+
+  string_print(original);
+  string_t *new = string_replace(original, substring_old, substring_new);
+  if (!new) {
+    printf("Invalid strings after substitution !");
+    return -3;
+  }
+
+  free(original);
+  free(substring_old);
+  free(substring_new);
+
+  string_print(new);
+  free(new);
+  return 0;
+}
+
+/**********************************************************************/
 
 string_t *string_colored(const char *str, enum stringcolor c) {
-  int n =  strlen(str) + strlen(COLOR_DEFAULT) + strlen(COLOR_BLACK);
+  int n = strlen(str) + strlen(COLOR_DEFAULT) + strlen(COLOR_BLACK);
   string_t *s = malloc(sizeof(string_t) + n);
-  if(unlikely(s == NULL)) return NULL;
+  if (unlikely(s == NULL))
+    return NULL;
   s->len = n;
+  // clang-format off
   switch(c) {
   case BLACK:   memcpy(s->buf,COLOR_BLACK,strlen(COLOR_BLACK));     break;
   case RED:     memcpy(s->buf,COLOR_RED,strlen(COLOR_RED));         break;
@@ -30,8 +86,9 @@ string_t *string_colored(const char *str, enum stringcolor c) {
   case WHITE:   memcpy(s->buf,COLOR_WHITE,strlen(COLOR_WHITE));     break;
   default: break;
   }
+  // clang-format on
   memcpy(&(s->buf[strlen(COLOR_BLACK)]), str, strlen(str));
-  n -=  strlen(COLOR_DEFAULT);
+  n -= strlen(COLOR_DEFAULT);
   memcpy(&(s->buf[n]), COLOR_DEFAULT, strlen(COLOR_DEFAULT));
   return s;
 }
@@ -40,7 +97,8 @@ string_t *string_colored(const char *str, enum stringcolor c) {
 
 string_t *string_nnew(const char *str, size_t len) {
   string_t *s = malloc(sizeof(string_t) + len);
-  if(unlikely(s == NULL)) return NULL;
+  if (unlikely(s == NULL))
+    return NULL;
   s->len = len;
   memcpy(s->buf, str, len);
   return s;
@@ -48,9 +106,7 @@ string_t *string_nnew(const char *str, size_t len) {
 
 /**********************************************************************/
 
-string_t *string_new(const char *str) {
-  return string_nnew(str, strlen(str));
-}
+string_t *string_new(const char *str) { return string_nnew(str, strlen(str)); }
 
 /**********************************************************************/
 
@@ -62,8 +118,9 @@ string_t *string_clone(const string_t *str) {
 
 string_t *string_readfd(int fd) {
   char buf[BUF_LEN];
-  int n = read(fd ,buf, BUF_LEN-1);
-  if(unlikely(n<0) ) return string_new("");
+  int n = read(fd, buf, BUF_LEN - 1);
+  if (unlikely(n < 0))
+    return string_new("");
   buf[n] = '\0';
   return string_new(buf);
 }
@@ -72,65 +129,71 @@ string_t *string_readfd(int fd) {
 
 string_t *string_readline(FILE *stream) {
   char buf[BUF_LEN];
-  if(!fgets(buf, BUF_LEN-1, stream)) return string_new("");
-  buf[strlen(buf)-1] = '\0';
+  if (!fgets(buf, BUF_LEN - 1, stream))
+    return string_new("");
+  buf[strlen(buf) - 1] = '\0';
   return string_new(buf);
 }
 
-
 /**********************************************************************/
 
 string_t *string_concat(const string_t *s1, const string_t *s2) {
   string_t *s = malloc(sizeof(string_t) + s1->len + s2->len);
-  if(unlikely(s == NULL)) return NULL;
+  if (unlikely(s == NULL))
+    return NULL;
   s->len = s1->len + s2->len;
   memcpy(s->buf, s1->buf, s1->len);
-  memcpy(s->buf+s1->len, s2->buf, s2->len);
+  memcpy(s->buf + s1->len, s2->buf, s2->len);
   return s;
 }
 
 /**********************************************************************/
 
 string_t *string_trim(const string_t *str) {
-  size_t l=0;
-  int r= str->len-1;
-  while(l < str->len && isspace(str->buf[l])) l+=1;
-  while(r>=0 && isspace(str->buf[r])) r-=1;
-  r+=1;
-  
-  if( unlikely(l> (size_t) r)) return string_new("");
+  size_t l = 0;
+  int r = str->len - 1;
+  while (l < str->len && isspace(str->buf[l]))
+    l += 1;
+  while (r >= 0 && isspace(str->buf[r]))
+    r -= 1;
+  r += 1;
+
+  if (unlikely(l > (size_t)r))
+    return string_new("");
 
-  return string_nnew( &(str->buf[l]), r-l);
+  return string_nnew(&(str->buf[l]), r - l);
 }
 
 /**********************************************************************/
 
 string_t *string_map(charfunc_t fun, const string_t *str) {
   string_t *s = string_clone(str);
-  if(unlikely(s == NULL)) return NULL;
-  for(size_t i=0;i<s->len;i++) {
+  if (unlikely(s == NULL))
+    return NULL;
+  for (size_t i = 0; i < s->len; i++) {
     s->buf[i] = fun(s->buf[i]);
   }
-  return s;                             
+  return s;
 }
 
 /**********************************************************************/
 
 string_t *string_filter(boolfunc_t fun, const string_t *str) {
-  int c=0;
+  int c = 0;
   char *tmp = malloc(str->len);
-  memcpy(tmp,str->buf,str->len);
-  for(size_t i=0; i < str->len; i++)
-    if(fun(str->buf[i])) tmp[c++] = str->buf[i]; 
+  memcpy(tmp, str->buf, str->len);
+  for (size_t i = 0; i < str->len; i++)
+    if (fun(str->buf[i]))
+      tmp[c++] = str->buf[i];
   tmp[c] = '\0';
   string_t *s = string_new(tmp);
   free(tmp);
-  return s;                             
+  return s;
 }
 
 /**********************************************************************/
 
-int string_compare(const string_t *s1,const string_t *s2) {
+int string_compare(const string_t *s1, const string_t *s2) {
   int n = (s1->len < s2->len) ? s1->len : s2->len;
   int r = strncmp(s1->buf, s2->buf, n);
 
@@ -140,40 +203,44 @@ int string_compare(const string_t *s1,const string_t *s2) {
 /**********************************************************************/
 
 bool string_equal(const string_t *s1, const string_t *s2) {
-  if(s1->len != s2->len) return false;
-  return strncmp(s1->buf,s2->buf,s1->len) == 0 ? true : false;   
+  if (s1->len != s2->len)
+    return false;
+  return strncmp(s1->buf, s2->buf, s1->len) == 0 ? true : false;
 }
 
 /**********************************************************************/
 
-string_t *string_substring(const string_t *str, size_t start, size_t end){
-  if(unlikely(!(start <= end) && (end <= str->len))) return NULL;
+string_t *string_substring(const string_t *str, size_t start, size_t end) {
+  if (unlikely(!(start <= end) && (end <= str->len)))
+    return NULL;
 
-  return string_nnew(&(str->buf[start]), end-start);
+  return string_nnew(&(str->buf[start]), end - start);
 }
 
 /**********************************************************************/
 
 string_t *string_repeat(const string_t *str, size_t times) {
-  size_t n =  str->len * times;
-  if( unlikely(!n)) return string_new("");
-  
+  size_t n = str->len * times;
+  if (unlikely(!n))
+    return string_new("");
+
   string_t *s = malloc(sizeof(string_t) + n);
-  if( unlikely(!s)) return NULL;
-  
+  if (unlikely(!s))
+    return NULL;
+
   s->len = n;
-  for(size_t i=0; i < times; i++)
-    memcpy(&(s->buf[i*(str->len)]), str->buf, str->len);
-  
+  for (size_t i = 0; i < times; i++)
+    memcpy(&(s->buf[i * (str->len)]), str->buf, str->len);
+
   return s;
 }
 
 /**********************************************************************/
 
-
 char *string_tocstr(const string_t *str) {
-  char *cstr = malloc(str->len +1);
-  if( unlikely(cstr==NULL)) return NULL;
+  char *cstr = malloc(str->len + 1);
+  if (unlikely(cstr == NULL))
+    return NULL;
   memcpy(cstr, str->buf, str->len);
   cstr[str->len] = '\0';
   return cstr;
@@ -181,48 +248,50 @@ char *string_tocstr(const string_t *str) {
 
 /**********************************************************************/
 
-static int string_substring_index_offset(const string_t *str, const string_t *substring, size_t offset) {
-  if(unlikely(substring->len == 0)) return offset;
-  if(unlikely(substring->len > (str->len - offset) )) return -1;
-
-  for(size_t i=offset; i<= str->len - substring->len; i++) {
-    for(size_t j=0; j < substring->len; j++) {
-      if(str->buf[i+j] != substring->buf[j]) break;
-      if( (j+1) == substring->len) return i;
+static int string_substring_index_offset(const string_t *str,
+                                         const string_t *substring,
+                                         size_t offset) {
+  if (unlikely(substring->len == 0))
+    return offset;
+  if (unlikely(substring->len > (str->len - offset)))
+    return -1;
+
+  for (size_t i = offset; i <= str->len - substring->len; i++) {
+    for (size_t j = 0; j < substring->len; j++) {
+      if (str->buf[i + j] != substring->buf[j])
+        break;
+      if ((j + 1) == substring->len)
+        return i;
     }
   }
   return -1;
 }
 
-
 int string_substring_index(const string_t *str, const string_t *substring) {
-  return string_substring_index_offset(str,substring, 0);
+  return string_substring_index_offset(str, substring, 0);
 }
 
-
 /**********************************************************************/
 
 bool string_is_substring(const string_t *str, const string_t *sub, size_t off) {
-  if(unlikely(sub->len+off > str->len)) return false;
-  if(unlikely(sub->len == 0)) return true;
+  if (unlikely(sub->len + off > str->len))
+    return false;
+  if (unlikely(sub->len == 0))
+    return true;
   return strncmp(&(str->buf[off]), sub->buf, sub->len) ? false : true;
-  
 }
 
-
-
 /**********************************************************************/
 
 string_t *string_replace_char(const string_t *str, char old, char new) {
-  string_t *s =  string_clone(str);
+  string_t *s = string_clone(str);
 
-  for(size_t i=0; i < s->len; i++) 
+  for (size_t i = 0; i < s->len; i++)
     s->buf[i] = (s->buf[i] == old) ? new : s->buf[i];
 
   return s;
 }
 
-
 /**********************************************************************/
 
 /*
@@ -230,91 +299,96 @@ string_t *string_replace_char(const string_t *str, char old, char new) {
  * suggestion by OpenAI's GPT-3.5
  */
 
-string_t *string_replace(const string_t *str, const string_t *old, const string_t *new) {
+string_t *string_replace(const string_t *str, const string_t *old,
+                         const string_t *new) {
   size_t n = 0;
   int offset = 0;
-  
-  while( (offset = string_substring_index_offset(str, old, offset)) > -1  ) {
-    offset+=old->len;
+
+  while ((offset = string_substring_index_offset(str, old, offset)) > -1) {
+    offset += old->len;
     n += 1;
   }
-  
-  if(n==0) return string_clone(str);
-  size_t len =  str->len + n * (new->len - old->len);
+
+  if (n == 0)
+    return string_clone(str);
+  size_t len = str->len + n * (new->len - old->len);
   string_t *s = malloc(sizeof(string_t) + len);
-  s->len = len;  
-  
+  // We add this check
+  if (!s) {
+    return s;
+  }
+  s->len = len;
+
   char *t = s->buf;
+
   int curr = 0;
-  offset=0;
-  while(n--) {
+  offset = 0;
+  while (n--) {
     offset = string_substring_index_offset(str, old, offset);
-    memcpy(t, str->buf+curr, offset-curr);
-    t += offset-curr;
+    memcpy(t, str->buf + curr, offset - curr);
+    t += offset - curr;
 
     memcpy(t, new->buf, new->len);
     t += new->len;
     curr = offset + old->len;
-    offset+=old->len;
+    offset += old->len;
   }
-  memcpy(t, str->buf+curr, str->len-curr);
-  
-  
+  memcpy(t, str->buf + curr, str->len - curr);
+
   return s;
 }
-  
-
 
 /**********************************************************************/
 
 string_vector_t *string_split(const string_t *str, char delimiter) {
   string_vector_t *svec = string_vector_empty();
   size_t start = 0;
-  for(size_t i=0; i< string_len(str); i++)
-    if(str->buf[i]==delimiter) {
-      string_vector_add(svec, string_nnew(&(str->buf[start]), i-start));
-      start = i+1;
+  for (size_t i = 0; i < string_len(str); i++)
+    if (str->buf[i] == delimiter) {
+      string_vector_add(svec, string_nnew(&(str->buf[start]), i - start));
+      start = i + 1;
     }
-  string_vector_add(svec, string_nnew(&(str->buf[start]), string_len(str)-start));
+  string_vector_add(svec,
+                    string_nnew(&(str->buf[start]), string_len(str) - start));
   return svec;
 }
 
-
 /**********************************************************************/
 
 string_vector_t *string_ssplit(const string_t *str, string_t *delimiter) {
   string_vector_t *svec = string_vector_empty();
   int idx = string_substring_index(str, delimiter);
-  if(idx==-1) {
+  if (idx == -1) {
     string_vector_add(svec, string_clone(str));
     return svec;
   }
   string_vector_add(svec, string_nnew(str->buf, idx));
-  idx += string_len(delimiter);  
-  
-  for(size_t i=idx; i<= string_len(str)-string_len(delimiter); i++) {
-    for(size_t j=0; str->buf[i+j] == delimiter->buf[j]; j++)
-      if( (j+1) == delimiter->len-1) {
-        string_vector_add(svec, string_nnew(&(str->buf[idx]), i-idx));
+  idx += string_len(delimiter);
+
+  for (size_t i = idx; i <= string_len(str) - string_len(delimiter); i++) {
+    for (size_t j = 0; str->buf[i + j] == delimiter->buf[j]; j++)
+      if ((j + 1) == delimiter->len - 1) {
+        string_vector_add(svec, string_nnew(&(str->buf[idx]), i - idx));
         idx = i + string_len(delimiter);
-        i += string_len(delimiter);  
+        i += string_len(delimiter);
         break;
       }
   }
-  if( (size_t) idx <= string_len(str))
-    string_vector_add(svec, string_nnew(&(str->buf[idx]), string_len(str)-idx));
-    
+  if ((size_t)idx <= string_len(str))
+    string_vector_add(svec,
+                      string_nnew(&(str->buf[idx]), string_len(str) - idx));
+
   return svec;
 }
 
-
 /*************************************************************************
  *                           String Vector                               *
  *************************************************************************/
 
-string_vector_t *string_vector_empty() {
+string_vector_t *string_vector_empty(void) {
   string_vector_t *svec = malloc(sizeof(string_vector_t));
-  if(unlikely(svec==NULL)) return NULL;
+  if (unlikely(svec == NULL))
+    return NULL;
   svec->buf = malloc(CAP_DEFAULT * sizeof(string_t *));
   svec->cap = CAP_DEFAULT;
   svec->top = -1;
@@ -323,28 +397,29 @@ string_vector_t *string_vector_empty() {
 
 string_vector_t *string_vector_new(string_t *str) {
   string_vector_t *svec = string_vector_empty();
-  if(unlikely(svec==NULL)) return NULL;
+  if (unlikely(svec == NULL))
+    return NULL;
   string_vector_add(svec, str);
   return svec;
 }
-  
+
 bool string_vector_is_empty(const string_vector_t *svec) {
-    return svec->top == -1;
+  return svec->top == -1;
 }
 
-
 void string_vector_free(string_vector_t *svec) {
   free(svec->buf);
   free(svec);
 }
 
-void string_vector_deepfree(string_vector_t *svec){
-  for(int i=0;i <= svec->top; i++) free(svec->buf[i]);
+void string_vector_deepfree(string_vector_t *svec) {
+  for (int i = 0; i <= svec->top; i++)
+    free(svec->buf[i]);
   string_vector_free(svec);
 }
 
 bool string_vector_is_full(string_vector_t *svec) {
-    return (size_t) (svec->top + 1) == svec->cap; 
+  return (size_t)(svec->top + 1) == svec->cap;
 }
 
 void string_vector_resize(string_vector_t *svec) {
@@ -353,52 +428,59 @@ void string_vector_resize(string_vector_t *svec) {
 }
 
 int string_vector_find(const string_vector_t *svec, const string_t *str) {
-  for(int i= 0; i<=svec->top; i++) 
-    if (string_equal(svec->buf[i] , str)) return i;
+  for (int i = 0; i <= svec->top; i++)
+    if (string_equal(svec->buf[i], str))
+      return i;
   return -1;
 }
 
-void string_vector_add(string_vector_t *svec,  string_t *str) {
-  if (string_vector_is_full(svec)) string_vector_resize(svec);
+void string_vector_add(string_vector_t *svec, string_t *str) {
+  if (string_vector_is_full(svec))
+    string_vector_resize(svec);
   svec->top += 1;
   svec->buf[svec->top] = str;
 }
 
-
 /**********************************************************************/
 
-
 string_t *string_vector_remove(string_vector_t *svec, size_t index) {
-  if ((int)index > svec->top) return NULL;
+  if ((int)index > svec->top)
+    return NULL;
   string_t *str = svec->buf[index];
-  for(int i=index; i<svec->top; i++) svec->buf[i] = svec->buf[i+1];
-  svec->top -=1;
+  for (int i = index; i < svec->top; i++)
+    svec->buf[i] = svec->buf[i + 1];
+  svec->top -= 1;
   return str;
 }
 
-
 /**********************************************************************/
 
 bool string_vector_equal(const string_vector_t *a, const string_vector_t *b) {
-  if(a->top != b->top) return false;
-  for(int i=0;i<=a->top;i++) if(!string_equal(a->buf[i],b->buf[i])) return false;
-  return true;   
+  if (a->top != b->top)
+    return false;
+  for (int i = 0; i <= a->top; i++)
+    if (!string_equal(a->buf[i], b->buf[i]))
+      return false;
+  return true;
 }
 
 /**********************************************************************/
 
 string_vector_t *string_vector_map(strfunc_t func,
                                    const string_vector_t *svec) {
-  if(string_vector_len(svec) == 0)  return string_vector_empty();
+  if (string_vector_len(svec) == 0)
+    return string_vector_empty();
 
   string_vector_t *res = malloc(sizeof(string_vector_t));
-  if(unlikely(!res)) return NULL;
+  if (unlikely(!res))
+    return NULL;
   res->buf = malloc(svec->cap * sizeof(string_t *));
   res->cap = svec->cap;
   res->top = svec->top;
   memcpy(res->buf, svec->buf, svec->top * sizeof(string_t *));
-  
-  for(int i = 0; i<= svec->top; i++) res->buf[i] = func(svec->buf[i]);
+
+  for (int i = 0; i <= svec->top; i++)
+    res->buf[i] = func(svec->buf[i]);
 
   return res;
 }
@@ -408,32 +490,29 @@ string_vector_t *string_vector_map(strfunc_t func,
 string_vector_t *string_vector_filter(strboolfunc_t func,
                                       const string_vector_t *svec) {
   string_vector_t *res = string_vector_empty();
-  if(unlikely(!res)) return NULL;
-  for(int i = 0; i<= svec->top; i++)
-    if(func(svec->buf[i])) string_vector_add(res, string_clone(svec->buf[i])); 
-  
-  return res;     
+  if (unlikely(!res))
+    return NULL;
+  for (int i = 0; i <= svec->top; i++)
+    if (func(svec->buf[i]))
+      string_vector_add(res, string_clone(svec->buf[i]));
+
+  return res;
 }
 
 /**********************************************************************/
 
-string_t *string_vector_reduce(reducefunc_t func,
-                               const string_vector_t *svec,
+string_t *string_vector_reduce(reducefunc_t func, const string_vector_t *svec,
                                string_t *initializer) {
   string_t *val = (initializer) ? string_clone(initializer) : string_new("");
-  
-  for(int i = 0; i<= svec->top; i++) {
-    string_t *t = func(val,svec->buf[i]);
+
+  for (int i = 0; i <= svec->top; i++) {
+    string_t *t = func(val, svec->buf[i]);
     free(val);
     val = t;
   }
   return val;
 }
 
-
 /**********************************************************************/
 
-
-const char *libstring_version() {
-  return LIBSTRING_VERSION;
-}
+const char *libstring_version() { return LIBSTRING_VERSION; }

config/libstring.h

 #pragma once
 
+#include <stdbool.h>
 #include <stdint.h>
 #include <stdio.h>
-#include <stdbool.h>
 #include <unistd.h>
 
 #define LIBSTRING_VERSION "0.1.3"
 
 #define COLOR_DEFAULT "\033[0m"
-#define COLOR_BLACK   "\033[30m"
-#define COLOR_RED     "\033[31m"
-#define COLOR_GREEN   "\033[32m"
-#define COLOR_YELLOW  "\033[33m"
-#define COLOR_BLUE    "\033[34m"
+#define COLOR_BLACK "\033[30m"
+#define COLOR_RED "\033[31m"
+#define COLOR_GREEN "\033[32m"
+#define COLOR_YELLOW "\033[33m"
+#define COLOR_BLUE "\033[34m"
 #define COLOR_MAGENTA "\033[35m"
-#define COLOR_CYAN    "\033[36m"
-#define COLOR_WHITE   "\033[37m"
+#define COLOR_CYAN "\033[36m"
+#define COLOR_WHITE "\033[37m"
 
-enum stringcolor {BLACK, RED, GREEN, YELLOW, BLUE, MAGENTA, CYAN, WHITE};
+enum stringcolor { BLACK, RED, GREEN, YELLOW, BLUE, MAGENTA, CYAN, WHITE };
 
 typedef struct {
   size_t len;
@@ -28,7 +28,8 @@ typedef struct {
  * Creates a new colored string_t initialized with the provided character array.
  *
  * @param str A null-terminated character array to initialize the string with.
- * @param c The color to apply to the string (specified by the enum stringcolor).
+ * @param c The color to apply to the string (specified by the enum
+ * stringcolor).
  * @return A pointer to the newly allocated and colored string containing a copy
  *         of the input character array, or NULL if memory allocation failed.
  *         The returned string must be deallocated using the standard C
@@ -36,7 +37,6 @@ typedef struct {
  */
 string_t *string_colored(const char *str, enum stringcolor c);
 
-
 /**
  * Allocates a new string_t initialized with the provided character array.
  *
@@ -48,7 +48,6 @@ string_t *string_colored(const char *str, enum stringcolor c);
  **/
 string_t *string_new(const char *str);
 
-
 /**
  * Creates a new string_t object as a copy of the provided string.
  *
@@ -61,7 +60,6 @@ string_t *string_new(const char *str);
  **/
 string_t *string_clone(const string_t *str);
 
-
 /**
  * Reads up to 64 KB of data from the specified file descriptor and
  * creates a new string containing the read data.
@@ -74,7 +72,6 @@ string_t *string_clone(const string_t *str);
  **/
 string_t *string_readfd(int fd);
 
-
 /**
  * Reads a line from a file stream, with a maximum of 64 KB of data,
  * and stores it as a newly allocated string.
@@ -87,7 +84,6 @@ string_t *string_readfd(int fd);
  **/
 string_t *string_readline(FILE *stream);
 
-
 /**
  * Concatenates two strings and returns a new string containing the combined
  * contents.
@@ -101,7 +97,6 @@ string_t *string_readline(FILE *stream);
  **/
 string_t *string_concat(const string_t *s1, const string_t *s2);
 
-
 /**
  * Creates a new string by removing leading and trailing whitespace characters
  * from the provided string.
@@ -132,15 +127,14 @@ int string_compare(const string_t *s1, const string_t *s2);
  * @return True if the contents of s1 are equal to the contents of s2, false
  *         otherwise.
  **/
-bool  string_equal(const string_t *s1, const string_t *s2);
-
+bool string_equal(const string_t *s1, const string_t *s2);
 
 /**
  * Creates a new string that represents a substring of the input string.
  *
  * @param str The input string.
  * @param start The starting index of the substring.
- * @param end The ending index of the substring 
+ * @param end The ending index of the substring
  * @return A pointer to a newly allocated string containing the specified
  *         substring, or NULL if memory allocation failed or NULL if the
  *         indices are out of bounds. The returned string must be deallocated
@@ -148,7 +142,6 @@ bool  string_equal(const string_t *s1, const string_t *s2);
  **/
 string_t *string_substring(const string_t *str, size_t start, size_t end);
 
-
 /**
  * Converts a string to a null-terminated C string.
  *
@@ -160,7 +153,6 @@ string_t *string_substring(const string_t *str, size_t start, size_t end);
  **/
 char *string_tocstr(const string_t *str);
 
-
 /**
  * Finds the first occurrence of a substring within a string.
  *
@@ -169,7 +161,7 @@ char *string_tocstr(const string_t *str);
  * @return The index of the first occurrence of the substring in the input
  *         string, or -1 if not found.
  **/
-int   string_substring_index(const string_t *str, const string_t *substring);
+int string_substring_index(const string_t *str, const string_t *substring);
 
 /**
  * Checks if a substring appears in the input string at a specified offset.
@@ -182,7 +174,6 @@ int   string_substring_index(const string_t *str, const string_t *substring);
  */
 bool string_is_substring(const string_t *str, const string_t *sub, size_t off);
 
-
 /**
  * Creates a new string by repeating the input string multiple times.
  *
@@ -198,7 +189,6 @@ bool string_is_substring(const string_t *str, const string_t *sub, size_t off);
  **/
 string_t *string_repeat(const string_t *str, size_t times);
 
-
 /**
  * Creates a new string where all occurrences of the 'old' character
  * in the input string are replaced with the 'new' character.
@@ -207,26 +197,28 @@ string_t *string_repeat(const string_t *str, size_t times);
  * @param old The character to be replaced.
  * @param new The character to replace occurrences of 'old'.
  * @return A new string with replaced characters. Must be freed after use.
- * @note The returned string is allocated on the heap and must be freed by the caller.
- * @note If 'old' is not found in the input string, the function returns a copy of the input string.
+ * @note The returned string is allocated on the heap and must be freed by the
+ *caller.
+ * @note If 'old' is not found in the input string, the function returns a copy
+ *of the input string.
  **/
 string_t *string_replace_char(const string_t *str, char old, char new);
 
-
-
- /* Creates a new string where all occurrences of the 'old' substring
+/* Creates a new string where all occurrences of the 'old' substring
  * in the input string are replaced with the 'new' substring.
  *
  * @param str The input string.
  * @param old The substring to be replaced.
  * @param new The substring to replace occurrences of 'old'.
  * @return A new string with replaced substrings. Must be freed after use.
- * @note The returned string is allocated on the heap and must be freed by the caller.
- * @note If 'old' is not found in the input string, the function returns a copy of the input string.
+ * @note The returned string is allocated on the heap and must be freed by the
+ *caller.
+ * @note If 'old' is not found in the input string, the function returns a copy
+ *of the input string.
  **/
-string_t *string_replace(const string_t *str, const string_t *old, const string_t *new);
+string_t *string_replace(const string_t *str, const string_t *old,
+                         const string_t *new);
 
-  
 /**
  * Returns the character at the specified index in the string.
  *
@@ -239,7 +231,6 @@ static inline char string_get(const string_t *s, size_t index) {
   return (index < s->len) ? s->buf[index] : -1;
 }
 
-
 /**
  * Reads a line from the standard input and stores it as a newly allocated
  * string.
@@ -249,10 +240,7 @@ static inline char string_get(const string_t *s, size_t index) {
  * must be deallocated using the standard C library function `free()` when no
  * longer needed.
  **/
-static inline string_t *string_read() {
-  return string_readfd(STDIN_FILENO);
-}
-
+static inline string_t *string_read() { return string_readfd(STDIN_FILENO); }
 
 /**
  * Reads a line from the specified file stream and stores it as a newly
@@ -264,21 +252,17 @@ static inline string_t *string_read() {
  *         deallocated using the standard C library function `free()` when no
  *         longer needed.
  **/
- static inline string_t *string_readf(FILE *stream) {
+static inline string_t *string_readf(FILE *stream) {
   return string_readfd(fileno(stream));
 }
 
-
 /**
  * Checks if the given string is empty (length is 0).
  *
  * @param s The string_t object to check.
  * @return true if the string is empty, false otherwise.
  */
-static inline bool string_empty(const string_t *s) {
-  return s->len == 0;
-}
-
+static inline bool string_empty(const string_t *s) { return s->len == 0; }
 
 /**
  * Returns the length (number of characters) of the string.
@@ -286,10 +270,7 @@ static inline bool string_empty(const string_t *s) {
  * @param s The string to get the length of.
  * @return The length of the string.
  */
-static inline size_t string_len(const string_t *s) {
-  return s->len;
-}
-
+static inline size_t string_len(const string_t *s) { return s->len; }
 
 /**
  * Prints the contents of the string to the standard output.
@@ -299,7 +280,7 @@ static inline size_t string_len(const string_t *s) {
  *         occurred.
  **/
 static inline int string_print(const string_t *s) {
-  return printf("%.*s", (int) s->len, s->buf);
+  return printf("%.*s", (int)s->len, s->buf);
 }
 
 /**
@@ -311,7 +292,7 @@ static inline int string_print(const string_t *s) {
  *         occurred.
  **/
 static inline int string_printf(const string_t *s, FILE *f) {
-  return fprintf(f, "%.*s", (int) s->len, s->buf);
+  return fprintf(f, "%.*s", (int)s->len, s->buf);
 }
 
 /**
@@ -323,7 +304,7 @@ static inline int string_printf(const string_t *s, FILE *f) {
  *         occurred.
  */
 static inline int string_println(const string_t *s) {
-  return printf("%.*s\n", (int) s->len, s->buf);
+  return printf("%.*s\n", (int)s->len, s->buf);
 }
 
 /**
@@ -336,11 +317,9 @@ static inline int string_println(const string_t *s) {
  *         occurred.
  */
 static inline int string_printlnf(const string_t *s, FILE *f) {
-  return fprintf(f, "%.*s\n", (int) s->len, s->buf);
+  return fprintf(f, "%.*s\n", (int)s->len, s->buf);
 }
 
-
-
 /**********************************************************************/
 
 typedef char (*charfunc_t)(char);
@@ -360,7 +339,6 @@ typedef bool (*boolfunc_t)(char);
  **/
 string_t *string_map(charfunc_t func, const string_t *str);
 
-
 /**
  * Filters the characters of the input string using a specified predicate
  * function.
@@ -375,16 +353,14 @@ string_t *string_map(charfunc_t func, const string_t *str);
  **/
 string_t *string_filter(boolfunc_t func, const string_t *str);
 
-
 /**********************************************************************
- *                        String Vector                               * 
+ *                        String Vector                               *
  **********************************************************************/
 
-
 typedef struct st_strvec {
   size_t cap;
   int top;
-  string_t **buf;  
+  string_t **buf;
 } string_vector_t;
 
 /**
@@ -400,7 +376,6 @@ typedef struct st_strvec {
  **/
 string_vector_t *string_split(const string_t *str, char delimiter);
 
-
 /**
  * Splits the given string into a vector of substrings based on the provided
  * delimiter.
@@ -418,8 +393,6 @@ string_vector_t *string_split(const string_t *str, char delimiter);
  **/
 string_vector_t *string_ssplit(const string_t *str, string_t *delimiter);
 
-
-
 /**
  * Creates an empty string_vector.
  *
@@ -427,8 +400,7 @@ string_vector_t *string_ssplit(const string_t *str, string_t *delimiter);
  *         memory allocation failed. The returned vector must be deallocated
  *         using `string_vector_free()` when no longer needed.
  **/
-string_vector_t *string_vector_empty();
-
+string_vector_t *string_vector_empty(void);
 
 /**
  * Creates a new string_vector initialized with the provided string.
@@ -461,9 +433,8 @@ void string_vector_free(string_vector_t *svec);
  **/
 void string_vector_deepfree(string_vector_t *svec);
 
-
 /**
- * Adds a string to a string_vector 
+ * Adds a string to a string_vector
  *
  * @param svec The string_vector_t object.
  * @param str The string to add.
@@ -494,7 +465,6 @@ int string_vector_find(const string_vector_t *svec, const string_t *str);
  **/
 string_t *string_vector_remove(string_vector_t *svec, size_t index);
 
-
 /**
  * Compares two string_vector objects for equality.
  *
@@ -505,7 +475,6 @@ string_t *string_vector_remove(string_vector_t *svec, size_t index);
  **/
 bool string_vector_equal(const string_vector_t *a, const string_vector_t *b);
 
-
 /**
  * Retrieves the string at the specified index from the string vector.
  * If the index is out of bounds, NULL is returned.
@@ -517,7 +486,7 @@ bool string_vector_equal(const string_vector_t *a, const string_vector_t *b);
  */
 static inline string_t *string_vector_get(const string_vector_t *svec,
                                           size_t index) {
-  return ((int) index > svec->top) ? NULL : svec->buf[index];
+  return ((int)index > svec->top) ? NULL : svec->buf[index];
 }
 
 /**
@@ -532,10 +501,9 @@ static inline size_t string_vector_len(const string_vector_t *svec) {
 
 /**********************************************************************/
 
-typedef string_t * (*strfunc_t)(string_t *);
+typedef string_t *(*strfunc_t)(string_t *);
 typedef bool (*strboolfunc_t)(string_t *);
-typedef string_t * (*reducefunc_t)(string_t *value, string_t *element);
-
+typedef string_t *(*reducefunc_t)(string_t *value, string_t *element);
 
 /**
  * Applies a function to each string in a string vector and creates a new
@@ -552,7 +520,6 @@ typedef string_t * (*reducefunc_t)(string_t *value, string_t *element);
  **/
 string_vector_t *string_vector_map(strfunc_t func, const string_vector_t *svec);
 
-
 /**
  * Filters the strings in a string vector object based on a filtering function.
  *
@@ -568,7 +535,6 @@ string_vector_t *string_vector_map(strfunc_t func, const string_vector_t *svec);
 string_vector_t *string_vector_filter(strboolfunc_t func,
                                       const string_vector_t *svec);
 
-
 /**
  * Filters the strings in a string vector based on a filtering function.
  *
@@ -604,14 +570,12 @@ string_vector_t *string_vector_filter(strboolfunc_t func,
  *         string vector. The returned string must be deallocated
  *         using the standard C library function `free()` when no longer needed.
  */
-string_t *string_vector_reduce(reducefunc_t func,
-                               const string_vector_t *svec,
+string_t *string_vector_reduce(reducefunc_t func, const string_vector_t *svec,
                                string_t *initializer);
 
-
 /**********************************************************************/
 
-/**  
+/**
  * Returns the version string of the libstring library.
  *
  * @return A pointer to the null-terminated version string.

flake.lock

+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1739736696,
+        "narHash": "sha256-zON2GNBkzsIyALlOCFiEBcIjI4w38GYOb+P+R4S8Jsw=",
+        "rev": "d74a2335ac9c133d6bbec9fc98d91a77f1604c1f",
+        "revCount": 754461,
+        "type": "tarball",
+        "url": "https://api.flakehub.com/f/pinned/NixOS/nixpkgs/0.1.754461%2Brev-d74a2335ac9c133d6bbec9fc98d91a77f1604c1f/01951426-5a87-7b75-8413-1a0d9ec5ff04/source.tar.gz"
+      },
+      "original": {
+        "type": "tarball",
+        "url": "https://flakehub.com/f/NixOS/nixpkgs/0.1.%2A.tar.gz"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

+{
+  description = "A Nix-flake-based C/C++ development environment";
+
+  inputs.nixpkgs.url = "https://flakehub.com/f/NixOS/nixpkgs/0.1.*.tar.gz";
+
+  outputs = { self, nixpkgs }:
+    let
+      supportedSystems = [ "x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin" ];
+      forEachSupportedSystem = f: nixpkgs.lib.genAttrs supportedSystems (system: f {
+        pkgs = import nixpkgs { inherit system; config.allowUnfree = true; };
+      });
+    in
+    {
+      devShells = forEachSupportedSystem ({ pkgs }: {
+        default = pkgs.mkShell.override
+          {
+            # Override stdenv in order to change compiler:
+            # stdenv = pkgs.clangStdenv;
+          }
+          {
+            packages = with pkgs; [
+              clang-tools
+	      framac
+	      clang
+	      gcc
+              cmake
+	      why3
+	      z3
+	      alt-ergo
+            ] ++ (if system == "aarch64-darwin" then [ ] else [ gdb ]);
+          };
+      });
+    };
+}
+