AdaCore/spark2014

Issues

• "Conversion error for node: unsupported base 1 for ureal" seemingly caused by Dimension_System

  #53 opened 15 days ago by liampwll
  2

• Fail to build on Linux arm64 - Long_Long_Float being 64 bits

  #54 opened 20 days ago by atupone
  12

• Building SPARK FSF 15 (fsf-15 branch) with LibGPR2 v25.0.0

  #51 opened 21 days ago by dvraaij
  2

• [FSF 15] Internal error for program allocating an array in a nested procedure.

  #55 opened 21 days ago by dvraaij
  2

• GNATprove crashes with GNAT bug on code with Address clause aliasing

  #52 opened 25 days ago by kittybwained
  3

• CVC5 unable to reason about "power" function

  #49 opened 3 months ago by rod-chapman
  8

• gnatprove bugs

  #50 opened 2 months ago by evanescente-ondine
  2

• gnatprove fails with gnatcoll as dependency in alire

  #48 opened 6 months ago by vbramselaar
  4

• Minor: `gnatprove --version` fails to show the version of Alt-Ergo.

  #43 opened a year ago by dvraaij
  4

• IPstack/AIP epoch. Year 2038 problem

  #47 opened a year ago by kevlar700
  0

• Issues with building the fsf-13 branch of SPARK with gnat-13

  #46 opened a year ago by dalybrown
  5

• Support for linux/arm64 in Host_Operating_System_Flavor

  #45 opened a year ago by dalybrown
  1

• Simple Sieve of Eratosthenes program triggers "(spark) GCC error: Error while reading SMT model ..."

  #41 opened 2 years ago by dev-muppet
  3

• SPARK gnatprove 12.1.1: segfault: Ada 2022 array 'Image attribute

  #40 opened 2 years ago by dev-muppet
  1

• Unsound handling of mod 16 bitwise negation

  #39 opened 3 years ago by ALPHA-60
  4

• Trying to build a set-up script for a Debian development box

  #35 opened 3 years ago by martin-cs
  1

• Colibri prover?

  #36 opened 3 years ago by simonjwright
  15

• FSF: unknown option '--giant-step-rac'

  #34 opened 3 years ago by simonjwright
  7

• GNAT bug box with fsf branch

  #32 opened 3 years ago by simonjwright
  3

• From_Universal_Image not present in FSF runtime

  #31 opened 3 years ago by kanigsson
  6

• fsf branch not building gnat2why

  #28 opened 3 years ago by simonjwright
  6

• Linking error of gnatvsn.o when building from source (FSF)

  #30 opened 3 years ago by 1ma
  2

• CONSTRAINT_ERROR raised when running gnat2why and spark_memcached_wrapper built from source (FSF)

  #29 opened 4 years ago by 1ma
  1

• Violation of GNATCheck rule 11.1.5.35

  #26 opened 4 years ago by pjljvandelaar
  3

• Strange traceback when running proof with gnatstudio from gnat-2021-20210519

  #27 opened 4 years ago by jcdubois
  3

• Wish: global and depends implicit annotations improvement.

  #16 opened 4 years ago by Blady-Com
  5

• fsf branch out of sync with FSF GCC ?

  #24 opened 5 years ago by steve-cs
  13

• bugbox triggered by Relaxed_Initialization variable used in aggregate

  #25 opened 4 years ago by faelys
  2

• Unsound handling of access type arguments

  #20 opened 5 years ago by tobycmurray
  8

• Handling of file specific proof switches?

  #23 opened 5 years ago by Jellix
  3

• fsf branch why3 build missing './install/libexec/spark/bin/' path

  #22 opened 5 years ago by steve-cs
  4

• gnat2why FSF build fails - "Ada_Text_IO_Child" is undefined

  #21 opened 5 years ago by steve-cs
  5

• developer guide: issues

  #19 opened 5 years ago by pjljvandelaar
  1

• Developer documentation seems to be missing

  #17 opened 5 years ago by pjljvandelaar
  4

• typos and wrong sentences

  #18 opened 5 years ago by pjljvandelaar
  1

• Manual Floating-Point proofs with gnatprove and Isabelle

  #13 opened 6 years ago by rasheedja
  3

• "Get_First_Main_File_Name" not declared in "Osint"

  #11 opened 6 years ago by Earnestly
  7

• SPARKSkein: check messages for potential problems

  #10 opened 6 years ago
  3

• build default target.atp

  #6 opened 6 years ago by anmaped
  6

• file "sa_messages.ads" not found

  #5 opened 7 years ago by Earnestly
  12

• gnatprove ignores -aP option

  #4 opened 7 years ago by atupone
  3

• Cannot prove with Coq

  #3 opened 7 years ago by mindbound
  2

• fmap.adb:304:18: "Null_FD" is undefined

  #2 opened 7 years ago by Earnestly
  3