Figure 1. Stepper Motor

A stepper motor controller emits a pulse which causes the motor to move one step. It seems simple, but in practice it turns out to be quite intricate to get right as one has to time the pulses individually to smoothly accelerate the rotation of the motor from a standing start until it reaches the some maximum velocity. Failure to do this will either limit the stepper motor to very low speed or result in skipped steps when the motor is under load. Similarly, a loaded motor must be slowly decelerated down to a stop.

Figure 2. Motion Profile

This implies the the width of the pulses must decrease as the motor accelerates. That is the pulse with has to be computed while the motor is in motion. This is illustrated in the above drawing. A program to accomplish this might look something like the following:

Already, this is turning it to a much more complex project than it first seemed. Searching around the net, we find a popular article on the operation of stepper motors using simple micro controllers. The algorithm is very well explained and it includes complete code we can test. The engineers are still debugging the prototype boards and hope to have them ready before the product actually ships. But this doesn't have to keep us from working on our code.

Inspecting this code, we find that it is written in a dialect of C rather than C itself. At the time this code was written, conforming versions of the C compiler were not available for PIC processors. We want to compile this code on the Microchip XC8 compiler which, for the most part, is standards conforming. So we made the following minimal changes:

The resulting program can be checked to be identical to the original but compiles on with the Microchip XC8 compiler. Given a development board, we could hook it up to a stepper motor, download and boot the code and verify that the motor rotates 5 revolutions in each direction with smooth acceleration and deceleration. We don't have such a board yet, but the engineers have promised a working board real soon now.

In order to develop our test suite and execute the same code on the desktop and the target system we factor out the shared code as a separate module which will used in both environments without change. The shared module motor2.c contains the algorithm for handling the interrupts in such a way as to create the smooth acceleration we require.

Using the target environment to run tests is often very difficult or impossible due to limited resources. So software unit testing for embedded systems is very problematic and often skipped. The C language on our desktop is the same used by the PIC18F2520. So now we can also run and debug the code on our desktop machine. Once our code passes all our tests, we can download the code to the embedded hardware and run the code natively. Here is a program we use on the desktop to do that:

//////////////////////////////////////////////////////////////////
// example92.cpp
//
// Copyright (c) 2015 Robert Ramey
//
// Distributed under the Boost Software License, Version 1.0. (See
// accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)

#include <iostream>

// *************************** 
// 1. include headers to support safe integers
#include <boost/safe_numerics/cpp.hpp>
#include <boost/safe_numerics/exception.hpp>
#include <boost/safe_numerics/safe_integer.hpp>

// *************************** 
// 2. specify a promotion policy to support proper emulation of 
// PIC types on the desktop
using pic16_promotion = boost::safe_numerics::cpp<
    8,  // char      8 bits
    16, // short     16 bits
    16, // int       16 bits
    16, // long      16 bits
    32  // long long 32 bits
>;

// 1st step=50ms; max speed=120rpm (based on 1MHz timer, 1.8deg steps)
#define C0    (50000 << 8)
#define C_MIN  (2500 << 8)

static_assert(C0 < 0xffffff, "Largest step too long");
static_assert(C_MIN > 0, "Smallest step must be greater than zero");
static_assert(C_MIN < C0, "Smallest step must be smaller than largest step");

// *************************** 
// 3. define PIC integer type names to be safe integer types of he same size.

template <typename T> // T is char, int, etc data type
using safe_t = boost::safe_numerics::safe<
    T,
    pic16_promotion
>;

// alias original program's integer types to corresponding PIC safe types
// In conjunction with the promotion policy above, this will permit us to 
// guarantee that the resulting program will be free of arithmetic errors 
// introduced by C expression syntax and type promotion with no runtime penalty

typedef safe_t<int8_t> int8;
typedef safe_t<int16_t> int16;
typedef safe_t<int32_t> int32;
typedef safe_t<uint8_t> uint8;
typedef safe_t<uint16_t> uint16;
typedef safe_t<uint32_t> uint32;

// *************************** 
// 4. emulate PIC features on the desktop

// filter out special keyword used only by XC8 compiler
#define __interrupt
// filter out XC8 enable/disable global interrupts
#define ei()
#define di()

// emulate PIC special registers
uint8 RCON;
uint8 INTCON;
uint8 CCP1IE;
uint8 CCP2IE;
uint8 PORTC;
uint8 TRISC;
uint8 T3CON;
uint8 T1CON;

uint8 CCPR2H;
uint8 CCPR2L;
uint8 CCPR1H;
uint8 CCPR1L;
uint8 CCP1CON;
uint8 CCP2CON;
uint8 TMR1H;
uint8 TMR1L;

// create type used to map PIC bit names to
// correct bit in PIC register
template<typename T, std::int8_t N>
struct bit {
    T & m_word;
    constexpr explicit bit(T & rhs) :
        m_word(rhs)
    {}
    constexpr bit & operator=(int b){
        if(b != 0)
            m_word |= (1 << N);
        else
            m_word &= ~(1 << N);
        return *this;
    }
    constexpr operator int () const {
        return m_word >> N & 1;
    }
};

// define bits for T1CON register
struct  {
    bit<uint8, 7> RD16{T1CON};
    bit<uint8, 5> T1CKPS1{T1CON};
    bit<uint8, 4> T1CKPS0{T1CON};
    bit<uint8, 3> T1OSCEN{T1CON};
    bit<uint8, 2> T1SYNC{T1CON};
    bit<uint8, 1> TMR1CS{T1CON};
    bit<uint8, 0> TMR1ON{T1CON};
} T1CONbits;

// define bits for T1CON register
struct  {
    bit<uint8, 7> GEI{INTCON};
    bit<uint8, 5> PEIE{INTCON};
    bit<uint8, 4> TMR0IE{INTCON};
    bit<uint8, 3> RBIE{INTCON};
    bit<uint8, 2> TMR0IF{INTCON};
    bit<uint8, 1> INT0IF{INTCON};
    bit<uint8, 0> RBIF{INTCON};
} INTCONbits;

// ***************************
// 5. include the environment independent code we want to test
#include "motor2.c"

#include <chrono>
#include <thread>

// round 24.8 format to microseconds
int32 to_microseconds(uint32 t){
    return (t + 128) / 256;
}

using result_t = uint8_t;
const result_t success = 1;
const result_t fail = 0;

// move motor to the indicated target position in steps
result_t test(int32 m){
    try {
        std::cout << "move motor to " << m << '\n';
        motor_run(m);
        std::cout
        << "step #" << ' '
        << "delay(us)(24.8)" << ' '
        << "delay(us)" << ' '
        << "CCPR" << ' '
        << "motor position" << '\n';
        do{
            std::this_thread::sleep_for(std::chrono::microseconds(to_microseconds(c)));
            uint32 last_c = c;
            uint32 last_ccpr = ccpr;
            isr_motor_step();
            std::cout
            << step_no << ' '
            << last_c << ' '
            << to_microseconds(last_c) << ' '
            << std::hex << last_ccpr << std::dec << ' '
            << motor_pos << '\n';
        }while(run_flg);
    }
    catch(const std::exception & e){
        std::cout << e.what() << '\n';
        return fail;
    }
    return success;
}

int main(){
    std::cout << "start test\n";
    result_t result = success;
    try{
        initialize();
        // move motor to position 1000
        result &= test(1000);
        // move motor to position 200
        result &= test(200);
        // move motor to position 200 again! Should result in no movement.
        result &= test(200);
        // move back to position 0
        result &= test(0);
        // ***************************
        // 6. error detected here!  data types can't handle enough
        // steps to move the carriage from end to end! Suppress this
        // test for now.
        // move motor to position 50000.
//        result &= test(50000);
        // move motor back to position 0.
        result &= test(0);
    }
    catch(const std::exception & e){
        std::cout << e.what() << '\n';
        return 1;
    }
    catch(...){
        std::cout << "test interrupted\n";
        return EXIT_FAILURE;
    }
    std::cout << "end test\n";
    return result == success ? EXIT_SUCCESS : EXIT_FAILURE;
}

Here are the essential features of the desktop version of the test program.

Our first attempt to run this program fails by throwing an exception from motor1.c indicating that the code attempts to left shift a negative number at the statements:

denom = ((step_no - move) << 2) + 1;

According to the C/C++ standards this is implementation defined behavior. But in practice with all modern platforms (as far as I know), this will be equivalent to a multiplication by 4. Clearly the intent of the original author is to "micro optimize" the operation by substituting a cheap left shift for a potentially expensive integer multiplication. But on all modern compilers, this substitution will be performed automatically by the compiler's optimizer. So we have two alternatives here:

Of these alternatives, the third seems the more definitive fix so we'll choose that one. We also decide to make a couple of minor changes to simplify the code and make mapping of the algorithm in the article to the code more transparent. With these changes, our test program runs to the end with no errors or exceptions. In addition, I made a minor change which simplifies the handling of floating point values in format of 24.8. This results in motor2.c which makes the above changes. It should be easy to see that these two versions are otherwise identical.

Finally our range test fails. In order to handle the full range we need, we'll have to change some data types used for holding step count and position. We won't do that here as it would make our example too complex. We'll deal with this on the next version.

We can test the same code we're going to load into our target system on the desktop. We could build and execute a complete unit test suite. We could capture the output and graph it. We have the ability to make are code much more likely to be bug free. But:

Can we catch all potential problems at compiler time and therefore eliminate all runtime cost?

Our first attempt consists of simply changing default exception policy from the default runtime checking to the compile time trapping one. Then we redefine the aliases for the types used by the PIC to use this exception policy.

// generate compile time errors if operation could fail 
using trap_policy = boost::numeric::loose_trap_policy;
...
typedef safe_t<int8_t, trap_policy> int8;
...

When we compile now, any expressions which could possibly fail will be flagged as syntax errors. This occurs 11 times when compiling the motor2.c program. This is fewer than one might expect. To understand why, consider the following example:

safe<std::int8_t> x, y;
...
safe<std::int16_t> z = x + y;

C promotion rules and arithmetic are such that the z will always contain an arithmetically correct result regardless of what values are assigned to x and y. Hence there is no need for any kind of checking of the arithmetic or result. The Safe Numerics library uses compile time range arithmetic, C++ template multiprogramming and other techniques to restrict invocation of checking code to only those operations which could possible fail. So the above code incurs no runtime overhead.

Now we have 11 cases to consider. Our goal is to modify the program so that this number of cases is reduced - hopefully to zero. Initially I wanted to just make a few tweaks in the versions of example92.c, motor2.c and motor_test2.c above without actually having to understand the code. It turns out that one needs to carefully consider what various types and variables are used for. This can be a good thing or a bad thing depending on one's circumstances, goals and personality. The programs above evolved into example93.c, motor3.c and motor_test3.c. First we'll look at example93.c:

//////////////////////////////////////////////////////////////////
// example93.cpp
//
// Copyright (c) 2015 Robert Ramey
//
// Distributed under the Boost Software License, Version 1.0. (See
// accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)

#include <iostream>

// include headers to support safe integers
#include <boost/safe_numerics/cpp.hpp>
#include <boost/safe_numerics/exception.hpp>
#include <boost/safe_numerics/safe_integer.hpp>
#include <boost/safe_numerics/safe_integer_range.hpp>
#include <boost/safe_numerics/safe_integer_literal.hpp>

// use same type promotion as used by the pic compiler
// target compiler XC8 supports:
using pic16_promotion = boost::safe_numerics::cpp<
    8,  // char      8 bits
    16, // short     16 bits
    16, // int       16 bits
    16, // long      16 bits
    32  // long long 32 bits
>;

// ***************************
// 1. Specify exception policies so we will generate a
// compile time error whenever an operation MIGHT fail.

// ***************************
// generate runtime errors if operation could fail
using exception_policy = boost::safe_numerics::default_exception_policy;

// generate compile time errors if operation could fail
using trap_policy = boost::safe_numerics::loose_trap_policy;

// ***************************
// 2. Create a macro named literal an integral value
// that can be evaluated at compile time.
#define literal(n) make_safe_literal(n, pic16_promotion, void)

// For min speed of 2 mm / sec (24.8 format)
// sec / step = sec / 2 mm * 2 mm / rotation * rotation / 200 steps
#define C0      literal(5000 << 8)

// For max speed of 400 mm / sec
// sec / step = sec / 400 mm * 2 mm / rotation * rotation / 200 steps
#define C_MIN   literal(25 << 8)

static_assert(
    C0 < make_safe_literal(0xffffff, pic16_promotion,trap_policy),
    "Largest step too long"
);
static_assert(
    C_MIN > make_safe_literal(0, pic16_promotion,trap_policy),
    "Smallest step must be greater than zero"
);

// ***************************
// 3. Create special ranged types for the motor program
// These wiil guarantee that values are in the expected
// ranges and permit compile time determination of when
// exceptional conditions might occur.

using pic_register_t = boost::safe_numerics::safe<
    uint8_t,
    pic16_promotion,
    trap_policy // use for compiling and running tests
>;

// note: the maximum value of step_t would be:
// 50000 = 500 mm / 2 mm/rotation * 200 steps/rotation.
// But in one expression the value of number of steps * 4 is
// used.  To prevent introduction of error, permit this
// type to hold the larger value.
using step_t = boost::safe_numerics::safe_unsigned_range<
    0,
    200000,
    pic16_promotion,
    exception_policy
>;

// position
using position_t = boost::safe_numerics::safe_unsigned_range<
    0,
    50000, // 500 mm / 2 mm/rotation * 200 steps/rotation
    pic16_promotion,
    exception_policy
>;

// next end of step timer value in format 24.8
// where the .8 is the number of bits in the fractional part.
using ccpr_t = boost::safe_numerics::safe<
    uint32_t,
    pic16_promotion,
    exception_policy
>;

// pulse length in format 24.8
// note: this value is constrainted to be a positive value. But
// we still need to make it a signed type. We get an arithmetic
// error when moving to a negative step number.
using c_t = boost::safe_numerics::safe_unsigned_range<
    C_MIN,
    C0,
    pic16_promotion,
    exception_policy
>;

// index into phase table
// note: The legal values are 0-3.  So why must this be a signed
// type?  Turns out that expressions like phase_ix + d
// will convert both operands to unsigned.  This in turn will
// create an exception.  So leave it signed even though the
// value is greater than zero.
using phase_ix_t = boost::safe_numerics::safe_signed_range<
    0,
    3,
    pic16_promotion,
    trap_policy
>;

// settings for control value output
using phase_t = boost::safe_numerics::safe<
    uint16_t,
    pic16_promotion,
    trap_policy
>;

// direction of rotation
using direction_t = boost::safe_numerics::safe_signed_range<
    -1,
    +1,
    pic16_promotion,
    trap_policy
>;

// some number of microseconds
using microseconds = boost::safe_numerics::safe<
    uint32_t,
    pic16_promotion,
    trap_policy
>;

// *************************** 
// emulate PIC features on the desktop

// filter out special keyword used only by XC8 compiler
#define __interrupt
// filter out XC8 enable/disable global interrupts
#define ei()
#define di()

// emulate PIC special registers
pic_register_t RCON;
pic_register_t INTCON;
pic_register_t CCP1IE;
pic_register_t CCP2IE;
pic_register_t PORTC;
pic_register_t TRISC;
pic_register_t T3CON;
pic_register_t T1CON;

pic_register_t CCPR2H;
pic_register_t CCPR2L;
pic_register_t CCPR1H;
pic_register_t CCPR1L;
pic_register_t CCP1CON;
pic_register_t CCP2CON;
pic_register_t TMR1H;
pic_register_t TMR1L;

// ***************************
// special checked type for bits - values restricted to 0 or 1
using safe_bit_t = boost::safe_numerics::safe_unsigned_range<
    0,
    1,
    pic16_promotion,
    trap_policy
>;

// create type used to map PIC bit names to
// correct bit in PIC register
template<typename T, std::int8_t N>
struct bit {
    T & m_word;
    constexpr explicit bit(T & rhs) :
        m_word(rhs)
    {}
    // special functions for assignment of literal
    constexpr bit & operator=(decltype(literal(1))){
        m_word |= literal(1 << N);
        return *this;
    }
    constexpr bit & operator=(decltype(literal(0))){
        m_word &= ~literal(1 << N);
        return *this;
    }
    // operator to convert to 0 or 1
    constexpr operator safe_bit_t () const {
        return m_word >> literal(N) & literal(1);
    }
};

// define bits for T1CON register
struct  {
    bit<pic_register_t, 7> RD16{T1CON};
    bit<pic_register_t, 5> T1CKPS1{T1CON};
    bit<pic_register_t, 4> T1CKPS0{T1CON};
    bit<pic_register_t, 3> T1OSCEN{T1CON};
    bit<pic_register_t, 2> T1SYNC{T1CON};
    bit<pic_register_t, 1> TMR1CS{T1CON};
    bit<pic_register_t, 0> TMR1ON{T1CON};
} T1CONbits;

// define bits for T1CON register
struct  {
    bit<pic_register_t, 7> GEI{INTCON};
    bit<pic_register_t, 5> PEIE{INTCON};
    bit<pic_register_t, 4> TMR0IE{INTCON};
    bit<pic_register_t, 3> RBIE{INTCON};
    bit<pic_register_t, 2> TMR0IF{INTCON};
    bit<pic_register_t, 1> INT0IF{INTCON};
    bit<pic_register_t, 0> RBIF{INTCON};
} INTCONbits;

#include "motor3.c"

#include <chrono>
#include <thread>

// round 24.8 format to microseconds
microseconds to_microseconds(ccpr_t t){
    return (t + literal(128)) / literal(256);
}

using result_t = uint8_t;
const result_t success = 1;
const result_t fail = 0;

// move motor to the indicated target position in steps
result_t test(position_t new_position){
    try {
        std::cout << "move motor to " << new_position << '\n';
        motor_run(new_position);
        std::cout
        << "step #" << ' '
        << "delay(us)(24.8)" << ' '
        << "delay(us)" << ' '
        << "CCPR" << ' '
        << "motor position" << '\n';
        while(busy()){
            std::this_thread::sleep_for(std::chrono::microseconds(to_microseconds(c)));
            c_t last_c = c;
            ccpr_t last_ccpr = ccpr;
            isr_motor_step();
            std::cout << i << ' '
            << last_c << ' '
            << to_microseconds(last_c) << ' '
            << std::hex << last_ccpr << std::dec << ' '
            << motor_position << '\n';
        };
    }
    catch(const std::exception & e){
        std::cout << e.what() << '\n';
        return fail;
    }
    return success;
}

int main(){
    std::cout << "start test\n";
    result_t result = success;
    try {
        initialize();
        // move motor to position 1000
        result &= test(literal(1000));
        // move to the left before zero position
        // fails to compile !
        // result &= ! test(-10);
        // move motor to position 200
        result &= test(literal(200));
        // move motor to position 200 again! Should result in no movement.
        result &= test(literal(200));
        // move motor to position 50000.
        result &= test(literal(50000));
        // move motor back to position 0.
        result &= test(literal(0));
    }
    catch(...){
        std::cout << "test interrupted\n";
        return EXIT_FAILURE;
    }
    std::cout << "end test\n";
    return result == success ? EXIT_SUCCESS : EXIT_FAILURE;
} 

Here are the changes we've made int the desktop test program

And we've made changes consistent with the above to motor3.c as well

/*
 * david austin
 * http://www.embedded.com/design/mcus-processors-and-socs/4006438/Generate-stepper-motor-speed-profiles-in-real-time
 * DECEMBER 30, 2004
 *
 * Demo program for stepper motor control with linear ramps
 * Hardware: PIC18F252, L6219
 *
 * Copyright (c) 2015 Robert Ramey
 *
 * Distributed under the Boost Software License, Version 1.0. (See
 * accompanying file LICENSE_1_0.txt or copy at
 * http://www.boost.org/LICENSE_1_0.txt)
 */

#include <assert.h>

// ramp state-machine states
enum ramp_state {
    ramp_idle = 0,
    ramp_up = 1,
    ramp_const = 2,
    ramp_down = 3,
};

// ***************************
// 1. Define state variables using custom strong types

// initial setup
enum ramp_state ramp_sts;
position_t motor_position;
position_t m;           // target position
position_t m2;          // midpoint or point where acceleration changes
direction_t d;          // direction of traval -1 or +1

// curent state along travel
step_t i;               // step number
c_t c;                  // 24.8 fixed point delay count increment
ccpr_t ccpr;            // 24.8 fixed point delay count
phase_ix_t phase_ix;    // motor phase index

// ***************************
// 2. Surround all literal values with the "literal" keyword

// Config data to make CCP1&2 generate quadrature sequence on PHASE pins
// Action on CCP match: 8=set+irq; 9=clear+irq
phase_t const ccpPhase[] = {
    literal(0x909),
    literal(0x908),
    literal(0x808),
    literal(0x809)
}; // 00,01,11,10

void current_on(){/* code as needed */}  // motor drive current
void current_off(){/* code as needed */} // reduce to holding value

// ***************************
// 3. Refactor code to make it easier to understand
// and relate to the documentation

bool busy(){
    return ramp_idle != ramp_sts;
}

// set outputs to energize motor coils
void update(ccpr_t ccpr, phase_ix_t phase_ix){
    // energize correct windings
    const phase_t phase = ccpPhase[phase_ix];
    CCP1CON = phase & literal(0xff); // set CCP action on next match
    CCP2CON = phase >> literal(8);
    // timer value at next CCP match
    CCPR1H = literal(0xff) & (ccpr >> literal(8));
    CCPR1L = literal(0xff) & ccpr;
}

// compiler-specific ISR declaration
// ***************************
// 4. Rewrite interrupt handler in a way which mirrors the orginal
// description of the algorithm and minimizes usage of state variable,
// accumulated values, etc.
void __interrupt isr_motor_step(void) { // CCP1 match -> step pulse + IRQ
    // *** possible exception
    // motor_position += d;
    // use the following to avoid mixing exception policies which is an error
    if(d < 0)
        --motor_position;
    else
        ++motor_position;
    // *** possible exception
    ++i;
    // calculate next difference in time
    for(;;){
        switch (ramp_sts) {
            case ramp_up: // acceleration
                if (i == m2) {
                    ramp_sts = ramp_down;
                    continue;
                }
                // equation 13
                // *** possible negative overflow on update of c
                c -= literal(2) * c / (literal(4) * i + literal(1));
                if(c < C_MIN){
                    c = C_MIN;
                    ramp_sts = ramp_const;
                    // *** possible exception
                    m2 = m - i; // new inflection point
                    continue;
                }
                break;
            case ramp_const: // constant speed
                if(i > m2) {
                    ramp_sts = ramp_down;
                    continue;
                }
                break;
            case ramp_down: // deceleration
                if (i == m) {
                    ramp_sts = ramp_idle;
                    current_off(); // reduce motor current to holding value
                    CCP1IE = literal(0); // disable_interrupts(INT_CCP1);
                    return;
                }
                // equation 14
                // *** possible positive overflow on update of c
                // note: re-arrange expression to avoid negative result
                // from difference of two unsigned values
                c += literal(2) * c / (literal(4) * (m - i) - literal(1));
                if(c > C0){
                    c = C0;
                }
                break;
            default:
                // should never arrive here!
                assert(false);
        } // switch (ramp_sts)
        break;
    }
    assert(c <= C0 && c >= C_MIN);
    // *** possible exception
    ccpr = literal(0xffffff) & (ccpr + c);
    phase_ix = (phase_ix + d) & literal(3);
    update(ccpr, phase_ix);
} // isr_motor_step()

// set up to drive motor to pos_new (absolute step#)
void motor_run(position_t new_position) {
    if(new_position > motor_position){
        d = literal(1);
        // *** possible exception
        m = new_position - motor_position;
    }
    else
    if(motor_position > new_position){
        d = literal(-1);
        // *** possible exception
        m = motor_position - new_position;
    }
    else{
        d = literal(0);
        m = literal(0);
        ramp_sts = ramp_idle; // start ramp state-machine
        return;
    }

    i = literal(0);
    m2 = m / literal(2);

    ramp_sts = ramp_up; // start ramp state-machine

    T1CONbits.TMR1ON = literal(0); // stop timer1;

    current_on(); // current in motor windings

    c = C0;
    ccpr = (TMR1H << literal(8) | TMR1L) + C0 + literal(1000);
    phase_ix = d & literal(3);
    update(ccpr, phase_ix);

    CCP1IE = literal(1); // enable_interrupts(INT_CCP1);
    T1CONbits.TMR1ON = literal(1); // restart timer1;
} // motor_run()

void initialize() {
    di();                // disable_interrupts(GLOBAL);
    motor_position = literal(0);
    CCP1IE = literal(0); // disable_interrupts(INT_CCP1);
    CCP2IE = literal(0); // disable_interrupts(INT_CCP2);
    PORTC = literal(0);  // output_c(0);
    TRISC = literal(0);  // set_tris_c(0);
    T3CON = literal(0);
    T1CON = literal(0x35);
    INTCONbits.PEIE = literal(1);
    INTCONbits.RBIF = literal(0);
    ei();                // enable_interrupts(GLOBAL);
} // initialize()

Finally we make a couple minor changes in motor_test3.c to verify that we can compile the exact same version of motor3.c on the PIC as well as on the desktop.

The intent of this case study is to show that the Safe Numerics Library can be an essential tool in validating the correctness of C/C++ programs in all environments - including the most restricted.

What we failed to do is to create a version of the program which uses the type system to prove that no results can be invalid. I turns out that states such as

++i;
c = f(c);

can't be proved not to overflow with this system. So we're left with having to depend upon exhaustive testing. It's not what we hoped, but it's the best we can do.