[Bug] Incorrect online execution result in SPARK tutorial (1/2)

Valutazione

Direzione di ricerca

Descrizione

> gnatprove -P main.gpr --checks-as-errors --level=0 --no-axiom-guard --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
show_map.adb:10:18: info: overflow check proved
show_map.adb:10:18: info: index check proved
show_map.adb:13:13: info: loop invariant preservation proved
show_map.adb:13:13: info: loop invariant initialization proved
show_map.adb:14:41: info: overflow check proved
show_map.adb:14:41: info: index check proved
show_map.adb:14:65: info: index check proved
show_map.adb:16:13: info: loop invariant initialization proved
show_map.adb:16:13: info: loop invariant preservation proved
show_map.adb:16:44: info: index check proved
show_map.adb:16:63: info: index check proved
show_map.adb:18:22: info: assertion proved
show_map.adb:19:50: info: overflow check proved
show_map.adb:19:50: info: index check proved
show_map.adb:19:65: info: index check proved
show_map.ads:8:35: info: overflow check proved
Summary logged in Courses.Intro_To_Spark.Proof_of_Functional_Correctness.Loop_Invariant_4/gnatprove/gnatprove.out

> gnatprove --version
SPARK Pro 23.0w (20220412)
Why3 for gnatprove version 1.4.1+git
alt-ergo: Alt-Ergo version 2.4.0
colibri: Colibri 2020.9
cvc4: This is CVC4 version 1.8
z3: Z3 version 4.8.15 - 64 bit

Preparare l'ambiente

Come iniziare

1. Leggi tutta la issue e poi la guida ai contributi del progetto.
2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
3. Fai un fork del repository e lavora su un branch.
4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di AdaCore/learn

• Custom_fixed_point_range.adb

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla
  question

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  AdaCore/learn#1238 · Aperta il 22/6/2025

• Startling name of chapter in "Introduction to SPARK": "Initialization of Local Variables"

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 1/5 Meno di un'ora Idoneità per principianti 35/100

  AdaCore/learn#1050 · Aperta il 14/5/2024

• Info messages are highlighted as errors when they have a reference to a second line and column numbers

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100

  AdaCore/learn#1049 · Aperta il 12/5/2024

• Inconsistent content between "Verification Method" and "Notes"

  Forse di nuovo libera @frank-at-adacore l’ha presa 897 giorni fa e non c’è nessuna pull request aperta. Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  AdaCore/learn#1041 · 1 commento · 1 assegnatario · Aperta il 2/5/2024

• warnings on code snippets are distracting attention from purpose

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  AdaCore/learn#917 · Aperta il 2/8/2023

Tutte le issue di AdaCore/learn

Issue simili

• [Sync EN] session_write_close(): fix the return value description (#5985)

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla
  sync-en

  Difficoltà 1/5 Meno di un'ora Idoneità per principianti 78/100

  php/doc-es#1486 · Aperta il 22/10/2026

  I maintainer di solito rispondono entro 2 giorni

• [oblt-aw][autodoc] Fix malformed headings in new Buildkite docs pages

  Forse già presa @github-actions l’ha presa oggi. Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla
  documentation

  Difficoltà 1/5 Meno di un'ora Idoneità per principianti 83/100

  elastic/oblt-aw#2426 · Aperta il 22/10/2026

  I maintainer di solito rispondono entro 1 giorno

• docs: kindle-formats.md quotes a 212 MB EPUB for the 304-page fixture; mangas kindle now writes 237 MB

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla
  documentation priority:p2 type:chore

  Difficoltà 2/5 1-3 ore Idoneità per principianti 73/100

  kerbaras/mangas#409 · Aperta il 22/10/2026

  I maintainer di solito rispondono entro 1 giorno

• docs(inventory): document router total and available interfaces

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla
  maintenance

  Difficoltà 2/5 1-3 ore Idoneità per principianti 68/100

  tyler-dalton/deployment-bags#25 · Aperta il 22/10/2026

• docs(ci): document repo-scope dispatch secret provisioning

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla
  dispatch:sol-high documentation

  Difficoltà 1/5 1-3 ore Idoneità per principianti 85/100

  carrick-sh/carrick#768 · 1 commento · Aperta il 22/10/2026

  I maintainer di solito rispondono entro 1 giorno

Altre issue su Documentation