Engine Test Front-end

This page is used to test the engine (front-end to backend interaction)

How it works

The test.js script reads the JSON descriptor listed before each test editor and simulates "pressing" the listed button. It then compares the response from the backend with the known 'test_expects' field. Insert new tests before the Test Results section at the end of the document.

Simple Ada Run Button Test

Simple Ada Run Button Test
Run...
Hello, World!
Success!
Run
with Ada.Text_IO; procedure Greet is begin -- Print "Hello, World!" to the screen Ada.Text_IO.Put_Line ("Hello, World!"); end Greet;

Simple C Run Button Test

Simple C Run Button Test
Run...
Hello, World!
Success!
Run
#include <stdio.h> int main() { printf("Hello, World!"); }

Accumulated Code Test

Accumulated Code Test
Run...
<Stack, items: [ 1 2 3 4]>
Success!
Run

package Var_Size_Record_2 is type Items_Array is array (Positive range <>) of Integer; type Growable_Stack (Max_Len : Natural) is record -- ^ Discriminant. Cannot be modified once initialized. Items : Items_Array (1 .. Max_Len); Len : Natural := 0; end record; -- Growable_Stack is an indefinite type (like an array) end Var_Size_Record_2;
with Var_Size_Record_2; use Var_Size_Record_2; with Ada.Text_IO; use Ada.Text_IO; procedure Main is procedure Print_Stack (G : Growable_Stack) is begin Put ("<Stack, items: ["); for I in G.Items'Range loop exit when I > G.Len; Put (" " & Integer'Image (G.Items (I))); end loop; Put_Line ("]>"); end Print_Stack; S : Growable_Stack := (Max_Len => 128, Items => (1, 2, 3, 4, others => <>), Len => 4); begin Print_Stack (S); end Main;

Examine SPARK Test

Examine SPARK Test
Examine...
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: analysis of data and information flow ...
show_uninitialized.adb:7:21: warning: "Max" may be referenced before it has a value
show_uninitialized.adb:7:21: medium: "Max" might not be initialized
show_uninitialized.adb:11:14: medium: "Max" might not be initialized
gnatprove: unproved check messages considered as errors
3 errors.
Examine
package Show_Uninitialized is type Array_Of_Naturals is array (Integer range <>) of Natural; function Max_Array (A : Array_Of_Naturals) return Natural; end Show_Uninitialized;
package body Show_Uninitialized is function Max_Array (A : Array_Of_Naturals) return Natural is Max : Natural; begin for I in A'Range loop if A (I) > Max then -- Here Max may not be initialized Max := A (I); end if; end loop; return Max; end Max_Array; end Show_Uninitialized;

Prove SPARK Test

Prove SPARK Test
Prove...
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
show_runtime_errors.adb:5:12: medium: overflow check might fail (e.g. when I = -2147483648 and J = -1)
show_runtime_errors.adb:5:12: medium: array index check might fail (e.g. when A'First = 1)
show_runtime_errors.adb:5:22: medium: range check might fail
show_runtime_errors.adb:5:22: medium: overflow check might fail (e.g. when P = -1 and Q = 0)
show_runtime_errors.adb:5:22: medium: divide by zero might fail (e.g. when Q = 0)
gnatprove: unproved check messages considered as errors
5 errors.
Prove
package Show_Runtime_Errors is type Nat_Array is array (Integer range <>) of Natural; procedure Update (A : in out Nat_Array; I, J, P, Q : Integer); end Show_Runtime_Errors;
package body Show_Runtime_Errors is procedure Update (A : in out Nat_Array; I, J, P, Q : Integer) is begin A (I + J) := P / Q; end Update; end Show_Runtime_Errors;

Test Results

placeholder text