Skip to content

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
#include <stdbool.h>
#include <stdint.h>
#include "WProgram.h"
int32_t notes[47] = {1519,1519,1519,1519,1519,1519,1519,1275,1915,1700,1519,1432,1432,1432,1432,1432,1519,1519,1519,1700,1700,1519,1700,1275,1519,1519,1519,1519,1519,1519,1519,1275,1915,1700,1519,1432,1432,1432,1432,1432,1519,1519,1275,1275,1432,1700,1915};
int32_t beats[47] = {1,1,2,1,1,2,1,1,1,1,4,1,1,1,1,1,1,2,1,1,1,1,2,2,1,1,2,1,1,2,1,1,1,1,4,1,1,1,1,1,1,2,1,1,1,1,4};
void playtone(int32_t , int32_t , int32_t);
static uint64_t __global_clock = 0;
struct { /* copilotStateCopilotSing */
struct { /* CopilotSing */
int32_t prophVal__idx[2];
bool playNote;
int32_t odd;
int32_t notes;
int32_t idx;
int32_t even;
int32_t duration;
uint64_t updateIndex__idx;
uint64_t outputIndex__idx;
int32_t tmpSampleVal__notes_Varidx;
int32_t tmpSampleVal__beats_Varidx;
} CopilotSing;
} copilotStateCopilotSing =
{ /* copilotStateCopilotSing */
{ /* CopilotSing */
/* prophVal__idx */
{ 0L
, 0L
},
/* playNote */ false,
/* odd */ 0L,
/* notes */ 0L,
/* idx */ 0L,
/* even */ 0L,
/* duration */ 0L,
/* updateIndex__idx */ 1ULL,
/* outputIndex__idx */ 0ULL,
/* tmpSampleVal__notes_Varidx */ 0L,
/* tmpSampleVal__beats_Varidx */ 0L
}
};
/* CopilotSing.updateOutput__playNote */
static void __r0() {
bool __0 = true;
if (__0) {
}
copilotStateCopilotSing.CopilotSing.playNote = __0;
}
/* CopilotSing.updateOutput__odd */
static void __r1() {
bool __0 = true;
uint64_t __1 = 0ULL;
uint64_t __2 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
uint64_t __3 = __1 + __2;
uint64_t __4 = 2ULL;
uint64_t __5 = __3 % __4;
int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__5];
int32_t __7 = 2L;
int32_t __8 = __6 % __7;
int32_t __9 = 1L;
bool __10 = __8 == __9;
int32_t __11 = 11L;
int32_t __12 = 12L;
int32_t __13 = __10 ? __11 : __12;
if (__0) {
}
copilotStateCopilotSing.CopilotSing.odd = __13;
}
/* CopilotSing.updateOutput__notes */
static void __r2() {
bool __0 = true;
int32_t __1 = copilotStateCopilotSing.CopilotSing.tmpSampleVal__notes_Varidx;
if (__0) {
}
copilotStateCopilotSing.CopilotSing.notes = __1;
}
/* CopilotSing.update__idx */
static void __r3() {
bool __0 = true;
uint64_t __1 = 0ULL;
uint64_t __2 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
uint64_t __3 = __1 + __2;
uint64_t __4 = 2ULL;
uint64_t __5 = __3 % __4;
int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__5];
int32_t __7 = 1L;
int32_t __8 = __6 + __7;
uint64_t __9 = copilotStateCopilotSing.CopilotSing.updateIndex__idx;
if (__0) {
}
copilotStateCopilotSing.CopilotSing.prophVal__idx[__9] = __8;
}
/* CopilotSing.updateOutput__even */
static void __r6() {
bool __0 = true;
uint64_t __1 = 0ULL;
uint64_t __2 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
uint64_t __3 = __1 + __2;
uint64_t __4 = 2ULL;
uint64_t __5 = __3 % __4;
int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__5];
int32_t __7 = 2L;
int32_t __8 = __6 % __7;
int32_t __9 = 1L;
bool __10 = __8 == __9;
int32_t __11 = 12L;
int32_t __12 = 11L;
int32_t __13 = __10 ? __11 : __12;
if (__0) {
}
copilotStateCopilotSing.CopilotSing.even = __13;
}
/* CopilotSing.updateOutput__duration */
static void __r7() {
bool __0 = true;
int32_t __1 = copilotStateCopilotSing.CopilotSing.tmpSampleVal__beats_Varidx;
int32_t __2 = 300L;
int32_t __3 = __1 * __2;
if (__0) {
}
copilotStateCopilotSing.CopilotSing.duration = __3;
}
/* CopilotSing.output__idx */
static void __r4() {
bool __0 = true;
uint64_t __1 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
uint64_t __2 = 1ULL;
uint64_t __3 = __1 + __2;
uint64_t __4 = 2ULL;
uint64_t __5 = __3 % __4;
int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__1];
if (__0) {
}
copilotStateCopilotSing.CopilotSing.outputIndex__idx = __5;
copilotStateCopilotSing.CopilotSing.idx = __6;
}
/* CopilotSing.trigger_playNote_playtone___const_13_notesduration_ */
static void __r8() {
bool __0 = copilotStateCopilotSing.CopilotSing.playNote;
if (__0) {
playtone(13 , copilotStateCopilotSing.CopilotSing.notes , copilotStateCopilotSing.CopilotSing.duration);
}
}
/* CopilotSing.trigger_playNote_digitalWrite__odd_const_1__ */
static void __r9() {
bool __0 = copilotStateCopilotSing.CopilotSing.playNote;
if (__0) {
digitalWrite(copilotStateCopilotSing.CopilotSing.odd , 1);
}
}
/* CopilotSing.trigger_playNote_digitalWrite__even_const_0__ */
static void __r10() {
bool __0 = copilotStateCopilotSing.CopilotSing.playNote;
if (__0) {
digitalWrite(copilotStateCopilotSing.CopilotSing.even , 0);
}
}
/* CopilotSing.sample__beats_Varidx */
static void __r11() {
bool __0 = true;
int32_t __1 = copilotStateCopilotSing.CopilotSing.idx;
int32_t __2 = beats[__1];
if (__0) {
}
copilotStateCopilotSing.CopilotSing.tmpSampleVal__beats_Varidx = __2;
}
/* CopilotSing.sample__notes_Varidx */
static void __r12() {
bool __0 = true;
int32_t __1 = copilotStateCopilotSing.CopilotSing.idx;
int32_t __2 = notes[__1];
if (__0) {
}
copilotStateCopilotSing.CopilotSing.tmpSampleVal__notes_Varidx = __2;
}
/* CopilotSing.incrUpdateIndex__idx */
static void __r5() {
bool __0 = true;
uint64_t __1 = copilotStateCopilotSing.CopilotSing.updateIndex__idx;
uint64_t __2 = 1ULL;
uint64_t __3 = __1 + __2;
uint64_t __4 = 2ULL;
uint64_t __5 = __3 % __4;
if (__0) {
}
copilotStateCopilotSing.CopilotSing.updateIndex__idx = __5;
}
void CopilotSing() {
{
static uint8_t __scheduling_clock = 0;
if (__scheduling_clock == 0) {
__r0(); /* CopilotSing.updateOutput__playNote */
__r1(); /* CopilotSing.updateOutput__odd */
__r2(); /* CopilotSing.updateOutput__notes */
__r3(); /* CopilotSing.update__idx */
__r6(); /* CopilotSing.updateOutput__even */
__r7(); /* CopilotSing.updateOutput__duration */
__scheduling_clock = 3;
}
else {
__scheduling_clock = __scheduling_clock - 1;
}
}
{
static uint8_t __scheduling_clock = 1;
if (__scheduling_clock == 0) {
__r4(); /* CopilotSing.output__idx */
__scheduling_clock = 3;
}
else {
__scheduling_clock = __scheduling_clock - 1;
}
}
{
static uint8_t __scheduling_clock = 2;
if (__scheduling_clock == 0) {
__r8(); /* CopilotSing.trigger_playNote_playtone___const_13_notesduration_ */
__r9(); /* CopilotSing.trigger_playNote_digitalWrite__odd_const_1__ */
__r10(); /* CopilotSing.trigger_playNote_digitalWrite__even_const_0__ */
__r11(); /* CopilotSing.sample__beats_Varidx */
__r12(); /* CopilotSing.sample__notes_Varidx */
__scheduling_clock = 3;
}
else {
__scheduling_clock = __scheduling_clock - 1;
}
}
{
static uint8_t __scheduling_clock = 3;
if (__scheduling_clock == 0) {
__r5(); /* CopilotSing.incrUpdateIndex__idx */
__scheduling_clock = 3;
}
else {
__scheduling_clock = __scheduling_clock - 1;
}
}
__global_clock = __global_clock + 1;
}
void playtone(int32_t speaker , int32_t tone , int32_t duration){
#ifdef CBMC
for (int32_t i = 0; i < 1; i ++) {
#else
for (int32_t i = 0; i < duration * 1000; i += tone * 2) {
#endif
digitalWrite(speaker, HIGH);
delayMicroseconds(tone);
digitalWrite(speaker, LOW);
delayMicroseconds(tone);
}
}
void setup(){
pinMode(13 , OUTPUT);
pinMode(12 , OUTPUT);
pinMode(11 , OUTPUT);
}
void loop(){
CopilotSing();
delay(3);
}
//Just for calling CBMC.
void cbmc(){
setup();
while(1) {
CopilotSing();
delay(3);
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.