package frama-c
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
  Platform dedicated to the analysis of source code written in C
Install
    
    dune-project
 Dependency
Authors
- 
  
    
    MMichele Alberti
- 
  
    
    TThibaud Antignac
- 
  
    
    GGergö Barany
- 
  
    
    PPatrick Baudin
- 
  
    
    NNicolas Bellec
- 
  
    
    TThibaut Benjamin
- 
  
    
    AAllan Blanchard
- 
  
    
    LLionel Blatter
- 
  
    
    FFrançois Bobot
- 
  
    
    RRichard Bonichon
- 
  
    
    VVincent Botbol
- 
  
    
    QQuentin Bouillaguet
- 
  
    
    DDavid Bühler
- 
  
    
    ZZakaria Chihani
- 
  
    
    SSylvain Chiron
- 
  
    
    LLoïc Correnson
- 
  
    
    JJulien Crétin
- 
  
    
    PPascal Cuoq
- 
  
    
    ZZaynah Dargaye
- 
  
    
    BBasile Desloges
- 
  
    
    JJean-Christophe Filliâtre
- 
  
    
    PPhilippe Herrmann
- 
  
    
    MMaxime Jacquemin
- 
  
    
    BBenjamin Jorge
- 
  
    
    FFlorent Kirchner
- 
  
    
    AAlexander Kogtenkov
- 
  
    
    RRemi Lazarini
- 
  
    
    TTristan Le Gall
- 
  
    
    KKilyan Le Gallic
- 
  
    
    JJean-Christophe Léchenet
- 
  
    
    MMatthieu Lemerre
- 
  
    
    DDara Ly
- 
  
    
    DDavid Maison
- 
  
    
    CClaude Marché
- 
  
    
    AAndré Maroneze
- 
  
    
    TThibault Martin
- 
  
    
    FFonenantsoa Maurica
- 
  
    
    MMelody Méaulle
- 
  
    
    BBenjamin Monate
- 
  
    
    YYannick Moy
- 
  
    
    PPierre Nigron
- 
  
    
    AAnne Pacalet
- 
  
    
    VValentin Perrelle
- 
  
    
    GGuillaume Petiot
- 
  
    
    DDario Pinto
- 
  
    
    VVirgile Prevosto
- 
  
    
    AArmand Puccetti
- 
  
    
    FFélix Ridoux
- 
  
    
    VVirgile Robles
- 
  
    
    JJan Rochel
- 
  
    
    MMuriel Roger
- 
  
    
    CCécile Ruet-Cros
- 
  
    
    JJulien Signoles
- 
  
    
    NNicolas Stouls
- 
  
    
    KKostyantyn Vorobyov
- 
  
    
    BBoris Yakobowski
Maintainers
Sources
  
    
      frama-c-31.0-Gallium.tar.gz
    
    
        
    
  
  
  
    
  
        sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567
    
    
  doc/qed/Qed/Kind/index.html
Module Qed.KindSource
Logic Types Utilities
Source
val tmap : 
  ('a, 'f) Logic.datatype array ->
  ('a, 'f) Logic.datatype ->
  ('a, 'f) Logic.datatypeSource
val pp_tau : 
  (Format.formatter -> int -> unit) ->
  (Format.formatter -> 'f -> unit) ->
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  ('f, 'a) Logic.datatype ->
  unitSource
val pp_data : 
  (Format.formatter -> 'a -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  'a ->
  'b list ->
  unitSource
val pp_record : 
  (Format.formatter -> 'f -> unit) ->
  (Format.formatter -> 'b -> unit) ->
  Format.formatter ->
  ?opened:bool ->
  ('f * 'b) list ->
  unitSource
val eq_tau : 
  ('f -> 'f -> bool) ->
  ('a -> 'a -> bool) ->
  ('f, 'a) Logic.datatype ->
  ('f, 'a) Logic.datatype ->
  boolSource
val compare_tau : 
  ('f -> 'f -> int) ->
  ('a -> 'a -> int) ->
  ('f, 'a) Logic.datatype ->
  ('f, 'a) Logic.datatype ->
  intSource
module MakeTau
  (F : Logic.Field)
  (A : Logic.Data) : 
  Logic.Data with type t = (F.t, A.t) Logic.datatype sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >